let R be Ring; :: thesis:
let I, K, L, i, k, l be Nat; :: thesis:
assume A1: i in Seg I ; :: thesis:
assume A2: k in Seg K ; :: thesis:
assume A3: l in Seg L ; :: thesis:
set LHS = (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R));
set RHS = canMat (i,l,I,L,R);

per cases ;

suppose I = 0 ; :: thesis:

hence (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R) by A1; :: thesis:

end;

suppose K = 0 ; :: thesis:

hence (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R) by A2; :: thesis:

end;

suppose L = 0 ; :: thesis:

hence (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R) by A3; :: thesis:

end;

suppose A4: ( I <> 0 & K <> 0 & L <> 0 ) ; :: thesis:

then A5: ( len (canMat (i,k,I,K,R)) = I & width (canMat (i,k,I,K,R)) = K & len (canMat (k,l,K,L,R)) = K & width (canMat (k,l,K,L,R)) = L ) by Th43;
then A6: width (canMat (i,k,I,K,R)) = len (canMat (k,l,K,L,R)) ;
A7: ( len ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) = len (canMat (i,l,I,L,R)) & width ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) = width (canMat (i,l,I,L,R)) )

proof

thus len ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) = I by A5, MATRIX_3:def 4
.= len (canMat (i,l,I,L,R)) by Th43 ; :: thesis:
thus width ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) = L by A5, MATRIX_3:def 4
.= width (canMat (i,l,I,L,R)) by A4, Th43 ; :: thesis:

end;

for i2, l2 being Nat st [i2,l2] in Indices ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) holds
((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) * (i2,l2) = (canMat (i,l,I,L,R)) * (i2,l2)

proof

let i2, l2 be Nat; :: thesis:
assume A8: [i2,l2] in Indices ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) ; :: thesis:
A9: ( i2 in Seg I & l2 in Seg L )

proof

A10: [i2,l2] in [:(dom ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)))),(Seg (width ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))))):] by A8, MATRIX_0:def 4;
dom ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) = Seg (len ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)))) by FINSEQ_1:def 3
.= Seg I by A5, MATRIX_3:def 4 ;
hence i2 in Seg I by A10, ZFMISC_1:87; :: thesis:
( i2 in dom ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) & l2 in Seg (width ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)))) ) by A10, ZFMISC_1:87;
hence l2 in Seg L by A5, MATRIX_3:def 4; :: thesis:

end;

A11: [i2,l2] in Indices (canMat (i,l,I,L,R))

proof

len (canMat (i,l,I,L,R)) = I by Th43;
then A12: i2 in dom (canMat (i,l,I,L,R)) by A9, FINSEQ_1:def 3;
width (canMat (i,l,I,L,R)) = L by A4, Th43;
then [i2,l2] in [:(dom (canMat (i,l,I,L,R))),(Seg (width (canMat (i,l,I,L,R)))):] by A9, A12, ZFMISC_1:87;
hence [i2,l2] in Indices (canMat (i,l,I,L,R)) by MATRIX_0:def 4; :: thesis:

end;

len (0. (R,K)) = K by MATRIX_0:25;
then A13: k in dom (0. (R,K)) by A2, FINSEQ_1:def 3;

per cases ;

suppose A14: i <> i2 ; :: thesis:

[i2,k] in Indices (canMat (i,k,I,K,R))

proof

len (canMat (i,k,I,K,R)) = I by Th43;
then A15: i2 in dom (canMat (i,k,I,K,R)) by A9, FINSEQ_1:def 3;
k in Seg (width (canMat (i,k,I,K,R))) by A2, A4, Th43;
then [i2,k] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A15, ZFMISC_1:87;
hence [i2,k] in Indices (canMat (i,k,I,K,R)) by MATRIX_0:def 4; :: thesis:

end;

then Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) by A14, Th44;
hence ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) * (i2,l2) = (Line ((0. (R,K)),k)) "*" (Col ((canMat (k,l,K,L,R)),l2)) by A6, A8, MATRIX_3:def 4
.= 0. R by A13, Th19
.= (canMat (i,l,I,L,R)) * (i2,l2) by A11, A14, Th40 ;
:: thesis:

end;

suppose A17: l2 <> l ; :: thesis:

[k,l2] in Indices (canMat (k,l,K,L,R))

proof

len (canMat (k,l,K,L,R)) = K by Th43;
then A18: k in dom (canMat (k,l,K,L,R)) by A2, FINSEQ_1:def 3;
l2 in Seg (width (canMat (k,l,K,L,R))) by A9, A4, Th43;
then [k,l2] in [:(dom (canMat (k,l,K,L,R))),(Seg (width (canMat (k,l,K,L,R)))):] by A18, ZFMISC_1:87;
hence [k,l2] in Indices (canMat (k,l,K,L,R)) by MATRIX_0:def 4; :: thesis:

end;

then A19: Col ((canMat (k,l,K,L,R)),l2) = Col ((0. (R,K)),k) by A17, Th45;
thus ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) * (i2,l2) = (Line ((canMat (i,k,I,K,R)),i2)) "*" (Col ((canMat (k,l,K,L,R)),l2)) by A6, A8, MATRIX_3:def 4
.= 0. R by A13, A19, Th20
.= (canMat (i,l,I,L,R)) * (i2,l2) by A11, A17, Th40 ; :: thesis:

end;

suppose A20: ( i = i2 & l = l2 ) ; :: thesis:

A21: ( k in dom (1. (R,K)) & k in dom (canMat (k,l,K,L,R)) )

proof

dom (1. (R,K)) = Seg (len (1. (R,K))) by FINSEQ_1:def 3
.= Seg K by MATRIX_0:24 ;
hence k in dom (1. (R,K)) by A2; :: thesis:
dom (canMat (k,l,K,L,R)) = Seg (len (canMat (k,l,K,L,R))) by FINSEQ_1:def 3
.= Seg K by Th43 ;
hence k in dom (canMat (k,l,K,L,R)) by A2; :: thesis:

end;

A22: [k,l] in Indices (canMat (k,l,K,L,R))

proof

len (canMat (k,l,K,L,R)) = K by Th43;
then A23: k in dom (canMat (k,l,K,L,R)) by A2, FINSEQ_1:def 3;
width (canMat (k,l,K,L,R)) = L by A4, Th43;
then [k,l] in [:(dom (canMat (k,l,K,L,R))),(Seg (width (canMat (k,l,K,L,R)))):] by A3, A23, ZFMISC_1:87;
hence [k,l] in Indices (canMat (k,l,K,L,R)) by MATRIX_0:def 4; :: thesis:

end;

[i2,k] in Indices (canMat (i,k,I,K,R))

proof

len (canMat (i,k,I,K,R)) = I by Th43;
then A24: i2 in dom (canMat (i,k,I,K,R)) by A9, FINSEQ_1:def 3;
width (canMat (i,k,I,K,R)) = K by A4, Th43;
then [i2,k] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A2, A24, ZFMISC_1:87;
hence [i2,k] in Indices (canMat (i,k,I,K,R)) by MATRIX_0:def 4; :: thesis:

end;

then A25: Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) by A20, Th44;
thus ((canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R))) * (i2,l2) = (Line ((canMat (i,k,I,K,R)),i2)) "*" (Col ((canMat (k,l,K,L,R)),l2)) by A6, A8, MATRIX_3:def 4
.= (canMat (k,l,K,L,R)) * (k,l2) by A21, A25, Th21
.= 1. R by A20, A22, Th40
.= (canMat (i,l,I,L,R)) * (i2,l2) by A20, A11, Th40 ; :: thesis:

end;

hence (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R) by A7, MATRIX_0:21; :: thesis:

end;