let R be Ring; :: thesis: for I, K, L being Nat st I <> 0 & K <> 0 holds
for i, k1, k2, l being Nat st k1 <> k2 holds
(canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L)
let I, K, L be Nat; :: thesis: ( I <> 0 & K <> 0 implies for i, k1, k2, l being Nat st k1 <> k2 holds
(canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L) )
assume A1: I <> 0 ; :: thesis: ( not K <> 0 or for i, k1, k2, l being Nat st k1 <> k2 holds
(canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L) )
assume A2: K <> 0 ; :: thesis: for i, k1, k2, l being Nat st k1 <> k2 holds
(canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L)
let i, k1, k2, l be Nat; :: thesis: ( k1 <> k2 implies (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L) )
assume A3: k1 <> k2 ; :: thesis: (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L)
set LHS = (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R));
set RHS = 0. (R,I,L);
A4: width (canMat (i,k1,I,K,R)) = K by A1, MATRIX_0:23
.= len (canMat (k2,l,K,L,R)) by MATRIX_0:25 ;
A5: ( (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) is Matrix of I,L,R & 0. (R,I,L) is Matrix of I,L,R )

proof

A6: len ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) = len (canMat (i,k1,I,K,R)) by A4, MATRIX_3:def 4
.= I by A1, MATRIX_0:23 ;
width ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) = width (canMat (k2,l,K,L,R)) by A4, MATRIX_3:def 4
.= L by A2, MATRIX_0:23 ;
hence ( (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) is Matrix of I,L,R & 0. (R,I,L) is Matrix of I,L,R ) by A1, A6, MATRIX_0:20; :: thesis: verum

end;

per cases ( not [i,k1] in Indices (canMat (i,k1,I,K,R)) or not [k2,l] in Indices (canMat (k2,l,K,L,R)) or ( [i,k1] in Indices (canMat (i,k1,I,K,R)) & [k2,l] in Indices (canMat (k2,l,K,L,R)) ) ) ;

suppose not [i,k1] in Indices (canMat (i,k1,I,K,R)) ; :: thesis: (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L)

then A7: canMat (i,k1,I,K,R) = 0. (R,I,K) by Th41;
( width (0. (R,I,K)) = K & width (canMat (k2,l,K,L,R)) = L & len (canMat (k2,l,K,L,R)) = K ) by A1, A2, MATRIX_0:23;
hence (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L) by A7, Th17; :: thesis: verum

end;

suppose not [k2,l] in Indices (canMat (k2,l,K,L,R)) ; :: thesis: (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L)

then A9: canMat (k2,l,K,L,R) = 0. (R,K,L) by Th41;
( len (canMat (i,k1,I,K,R)) = I & width (canMat (i,k1,I,K,R)) = K & width (0. (R,K,L)) = L ) by A1, A2, MATRIX_0:23;
hence (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L) by A9, Th18; :: thesis: verum

end;

suppose A11: ( [i,k1] in Indices (canMat (i,k1,I,K,R)) & [k2,l] in Indices (canMat (k2,l,K,L,R)) ) ; :: thesis: (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L)

for i9, l9 being Nat st [i9,l9] in Indices ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) holds
((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) * (i9,l9) = (0. (R,I,L)) * (i9,l9)

proof

let i9, l9 be Nat; :: thesis: ( [i9,l9] in Indices ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) implies ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) * (i9,l9) = (0. (R,I,L)) * (i9,l9) )
assume A12: [i9,l9] in Indices ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) ; :: thesis: ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) * (i9,l9) = (0. (R,I,L)) * (i9,l9)
then [i9,l9] in [:(Seg I),(Seg L):] by A1, A5, MATRIX_0:23;
then A13: ( i9 in Seg I & l9 in Seg L ) by ZFMISC_1:87;
A14: [i9,k1] in Indices (canMat (i,k1,I,K,R))

proof

[i9,l9] in [:(dom ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)))),(Seg (width ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))))):] by A12, MATRIX_0:def 4;
then i9 in dom ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) by ZFMISC_1:87;
then i9 in Seg (len ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)))) by FINSEQ_1:def 3;
then i9 in Seg (len (canMat (i,k1,I,K,R))) by A4, MATRIX_3:def 4;
then A15: i9 in dom (canMat (i,k1,I,K,R)) by FINSEQ_1:def 3;
[i,k1] in [:(dom (canMat (i,k1,I,K,R))),(Seg (width (canMat (i,k1,I,K,R)))):] by A11, MATRIX_0:def 4;
then ( i in dom (canMat (i,k1,I,K,R)) & k1 in Seg (width (canMat (i,k1,I,K,R))) ) by ZFMISC_1:87;
then [i9,k1] in [:(dom (canMat (i,k1,I,K,R))),(Seg (width (canMat (i,k1,I,K,R)))):] by A15, ZFMISC_1:87;
hence [i9,k1] in Indices (canMat (i,k1,I,K,R)) by MATRIX_0:def 4; :: thesis: verum

end;

then [i9,k1] in [:(Seg I),(Seg K):] by A1, MATRIX_0:23;
then A16: ( i9 in Seg I & k1 in Seg K ) by ZFMISC_1:87;
A17: [i9,l9] in Indices (0. (R,I,L))

proof

[i9,l9] in [:(Seg I),(Seg L):] by A13, ZFMISC_1:87;
hence [i9,l9] in Indices (0. (R,I,L)) by A1, MATRIX_0:23; :: thesis: verum

end;

k1 in Seg (len (canMat (k2,l,K,L,R))) by A2, A16, MATRIX_0:23;
then A18: k1 in dom (canMat (k2,l,K,L,R)) by FINSEQ_1:def 3;
A19: [k1,l9] in Indices (canMat (k2,l,K,L,R))

proof

[k1,l9] in [:(Seg K),(Seg L):] by A13, A16, ZFMISC_1:87;
hence [k1,l9] in Indices (canMat (k2,l,K,L,R)) by A2, MATRIX_0:23; :: thesis: verum

end;

Indices (canMat (i,k1,I,K,R)) = [:(Seg I),(Seg K):] by A1, MATRIX_0:23;
then k1 in Seg K by A11, ZFMISC_1:87;
then k1 in Seg (len (1. (R,K))) by MATRIX_0:24;
then A20: k1 in dom (1. (R,K)) by FINSEQ_1:def 3;
A21: dom (1. (R,K)) = Seg (len (1. (R,K))) by FINSEQ_1:def 3
.= Seg K by MATRIX_0:24
.= Seg (len (0. (R,K))) by MATRIX_0:24
.= dom (0. (R,K)) by FINSEQ_1:def 3 ;

per cases ( i9 = i or i9 <> i ) ;

suppose A22: i9 = i ; :: thesis: ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) * (i9,l9) = (0. (R,I,L)) * (i9,l9)

thus ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) * (i9,l9) = (Line ((canMat (i,k1,I,K,R)),i9)) "*" (Col ((canMat (k2,l,K,L,R)),l9)) by A4, A12, MATRIX_3:def 4
.= (Line ((1. (R,K)),k1)) "*" (Col ((canMat (k2,l,K,L,R)),l9)) by A22, A14, Th44
.= (canMat (k2,l,K,L,R)) * (k1,l9) by A20, A18, Th21
.= 0. R by A3, A19, Th40
.= (0. (R,I,L)) * (i9,l9) by A17, MATRIX_3:1 ; :: thesis: verum

end;

suppose A23: i9 <> i ; :: thesis: ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) * (i9,l9) = (0. (R,I,L)) * (i9,l9)

thus ((canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R))) * (i9,l9) = (Line ((canMat (i,k1,I,K,R)),i9)) "*" (Col ((canMat (k2,l,K,L,R)),l9)) by A4, A12, MATRIX_3:def 4
.= (Line ((0. (R,K)),k1)) "*" (Col ((canMat (k2,l,K,L,R)),l9)) by A23, A14, Th44
.= 0. R by A20, A21, Th19
.= (0. (R,I,L)) * (i9,l9) by A17, MATRIX_3:1 ; :: thesis: verum

end;

end;

end;

hence (canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L) by A5, MATRIX_0:27; :: thesis: verum

end;

end;