Note that it is necessary that all of the equations in the spreadsheet have solutions, since they are implied by the original equations. The equations involving only knowns play a key role. In particular, they say precisely that, there must exist a projection such that

are satisfied.

The converse is also true and can be verified with the assistance
of the above spreadsheet.
To do this, we assume that
the matrices *A*, *B*, *C* and are given
and that (theTwoEquations) holds, and wish
to define , , , , *a*,
*b*, *c*, *e*, *f* and *g* such that each of the
equations in the above spreadsheet hold. If we can do this,
then each of the equations from the starting polynomial equations
(*FAC*) given in §subsection:problem will hold
and we will have shown that
a minimal factorization of
the [*A*,*B*,*C*,1] system exists.

- (1) Since , it is easy to show that there exists (not necessarily square) matrices and such that and . These are exactly the equations in the -Category of the above spreadsheet.
- (2) Since , it is easy to show that there exists (not necessarily square) matrices and such that and . These are exactly the equations in the -Category of the above spreadsheet together with the equations in the -Category of the above spreadsheet.
- (3) Since we have defined , , and
, we can define
*a*,*b*,*c*,*e*,*f*and*g*by setting , , , , and . These are exactly the equations in the singleton category.

With the assignments made above, every equation in the spreadsheet
above holds.
Thus, by backsolving through the spreadsheet,
we have constructed the factors of the
original system [*A*,*B*,*C*,1].
This proves

**Theorem ([BGKvD])**
The system [*A*, *B*, *C*, 1] can be factored if and only if there exists a projection
such that and
.

Note that the known equations can be neatly expressed in terms of and . Indeed, it is easy to check with a little algebra that these are equivalent to (eq:answer). It is a question of taste, not algebra, as to which form one chooses.

For a more complicated example of an end game, see §.

Wed Jul 3 10:27:42 PDT 1996