let R be Ring; :: thesis: for I, K, i, k, k2 being Nat st [i,k2] in Indices (canMat (i,k,I,K,R)) holds
( ( k2 = k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((1. (R,I)),i) ) & ( k2 <> k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((0. (R,I)),i) ) )
let I, K, i, k, k2 be Nat; :: thesis: ( [i,k2] in Indices (canMat (i,k,I,K,R)) implies ( ( k2 = k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((1. (R,I)),i) ) & ( k2 <> k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((0. (R,I)),i) ) ) )
assume A1: [i,k2] in Indices (canMat (i,k,I,K,R)) ; :: thesis: ( ( k2 = k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((1. (R,I)),i) ) & ( k2 <> k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((0. (R,I)),i) ) )
A2: dom (canMat (i,k,I,K,R)) = Seg (len (canMat (i,k,I,K,R))) by FINSEQ_1:def 3
.= Seg I by Th43 ;
A3: dom (Col ((canMat (i,k,I,K,R)),k2)) = Seg (len (Col ((canMat (i,k,I,K,R)),k2))) by FINSEQ_1:def 3
.= Seg (len (canMat (i,k,I,K,R))) by MATRIX_0:def 8
.= Seg I by Th43 ;
A4: ( i in dom (canMat (i,k,I,K,R)) & k2 in Seg (width (canMat (i,k,I,K,R))) )

proof

[i,k2] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A1, MATRIX_0:def 4;
hence ( i in dom (canMat (i,k,I,K,R)) & k2 in Seg (width (canMat (i,k,I,K,R))) ) by ZFMISC_1:87; :: thesis: verum

end;

A5: for j9 being Nat st j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) holds
[j9,k2] in Indices (canMat (i,k,I,K,R))

proof

let j9 be Nat; :: thesis: ( j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) implies [j9,k2] in Indices (canMat (i,k,I,K,R)) )
assume A6: j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) ; :: thesis: [j9,k2] in Indices (canMat (i,k,I,K,R))
dom (Col ((canMat (i,k,I,K,R)),k2)) = Seg (len (Col ((canMat (i,k,I,K,R)),k2))) by FINSEQ_1:def 3
.= dom (canMat (i,k,I,K,R)) by FINSEQ_1:def 3, MATRIX_0:def 8 ;
then [j9,k2] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A4, A6, ZFMISC_1:87;
hence [j9,k2] in Indices (canMat (i,k,I,K,R)) by MATRIX_0:def 4; :: thesis: verum

end;

A7: for j9 being Nat st j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) holds
[j9,i] in Indices (1. (R,I))

proof

let j9 be Nat; :: thesis: ( j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) implies [j9,i] in Indices (1. (R,I)) )
assume j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) ; :: thesis: [j9,i] in Indices (1. (R,I))
then [j9,i] in [:(Seg I),(Seg I):] by A2, A3, A4, ZFMISC_1:87;
hence [j9,i] in Indices (1. (R,I)) by MATRIX_0:24; :: thesis: verum

end;

thus ( k2 = k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((1. (R,I)),i) ) :: thesis: ( k2 <> k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((0. (R,I)),i) )

proof

assume A8: k2 = k ; :: thesis: Col ((canMat (i,k,I,K,R)),k2) = Col ((1. (R,I)),i)
A9: dom (Col ((canMat (i,k,I,K,R)),k2)) = Seg (len (1. (R,I))) by A3, MATRIX_0:24
.= Seg (len (Col ((1. (R,I)),i))) by MATRIX_0:def 8
.= dom (Col ((1. (R,I)),i)) by FINSEQ_1:def 3 ;
for j9 being Nat st j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) holds
(Col ((canMat (i,k,I,K,R)),k2)) . j9 = (Col ((1. (R,I)),i)) . j9

proof

let j9 be Nat; :: thesis: ( j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) implies (Col ((canMat (i,k,I,K,R)),k2)) . j9 = (Col ((1. (R,I)),i)) . j9 )
assume A10: j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) ; :: thesis: (Col ((canMat (i,k,I,K,R)),k2)) . j9 = (Col ((1. (R,I)),i)) . j9
then A11: [j9,k2] in Indices (canMat (i,k,I,K,R)) by A5;
A12: [j9,i] in Indices (1. (R,I)) by A10, A7;
then [j9,i] in [:(dom (1. (R,I))),(Seg (width (1. (R,I)))):] by MATRIX_0:def 4;
then A13: j9 in dom (1. (R,I)) by ZFMISC_1:87;

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

suppose A14: j9 = i ; :: thesis: (Col ((canMat (i,k,I,K,R)),k2)) . j9 = (Col ((1. (R,I)),i)) . j9

thus (Col ((canMat (i,k,I,K,R)),k2)) . j9 = (canMat (i,k,I,K,R)) * (j9,k2) by A2, A3, A10, MATRIX_0:def 8
.= 1. R by A8, A11, A14, Th40
.= (1. (R,I)) * (j9,i) by A12, A14, MATRIX_1:def 3
.= (Col ((1. (R,I)),i)) . j9 by A13, MATRIX_0:def 8 ; :: thesis: verum

end;

suppose A15: j9 <> i ; :: thesis: (Col ((canMat (i,k,I,K,R)),k2)) . j9 = (Col ((1. (R,I)),i)) . j9

thus (Col ((canMat (i,k,I,K,R)),k2)) . j9 = (canMat (i,k,I,K,R)) * (j9,k2) by A2, A3, A10, MATRIX_0:def 8
.= 0. R by A11, A15, Th40
.= (1. (R,I)) * (j9,i) by A12, A15, MATRIX_1:def 3
.= (Col ((1. (R,I)),i)) . j9 by A13, MATRIX_0:def 8 ; :: thesis: verum

end;

end;

end;

hence Col ((canMat (i,k,I,K,R)),k2) = Col ((1. (R,I)),i) by A9, FINSEQ_1:13; :: thesis: verum

end;

assume A16: k2 <> k ; :: thesis: Col ((canMat (i,k,I,K,R)),k2) = Col ((0. (R,I)),i)
A17: for j9 being Nat st j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) holds
[j9,i] in Indices (0. (R,I))

proof

let j9 be Nat; :: thesis: ( j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) implies [j9,i] in Indices (0. (R,I)) )
assume j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) ; :: thesis: [j9,i] in Indices (0. (R,I))
then [j9,i] in [:(Seg I),(Seg I):] by A2, A3, A4, ZFMISC_1:87;
hence [j9,i] in Indices (0. (R,I)) by MATRIX_0:24; :: thesis: verum

end;

A18: dom (Col ((canMat (i,k,I,K,R)),k2)) = Seg (len (0. (R,I))) by A3, MATRIX_0:24
.= Seg (len (Col ((0. (R,I)),i))) by MATRIX_0:def 8
.= dom (Col ((0. (R,I)),i)) by FINSEQ_1:def 3 ;
for j9 being Nat st j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) holds
(Col ((canMat (i,k,I,K,R)),k2)) . j9 = (Col ((0. (R,I)),i)) . j9

proof

let j9 be Nat; :: thesis: ( j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) implies (Col ((canMat (i,k,I,K,R)),k2)) . j9 = (Col ((0. (R,I)),i)) . j9 )
assume A19: j9 in dom (Col ((canMat (i,k,I,K,R)),k2)) ; :: thesis: (Col ((canMat (i,k,I,K,R)),k2)) . j9 = (Col ((0. (R,I)),i)) . j9
A20: [j9,k2] in Indices (canMat (i,k,I,K,R)) by A5, A19;
A21: [j9,i] in Indices (0. (R,I)) by A19, A17;
then [j9,i] in [:(dom (0. (R,I))),(Seg (width (0. (R,I)))):] by MATRIX_0:def 4;
then A22: j9 in dom (0. (R,I)) by ZFMISC_1:87;
thus (Col ((canMat (i,k,I,K,R)),k2)) . j9 = (canMat (i,k,I,K,R)) * (j9,k2) by A2, A3, A19, MATRIX_0:def 8
.= 0. R by A20, A16, Th40
.= (0. (R,I)) * (j9,i) by A21, MATRIX_1:1
.= (Col ((0. (R,I)),i)) . j9 by A22, MATRIX_0:def 8 ; :: thesis: verum

end;

hence Col ((canMat (i,k,I,K,R)),k2) = Col ((0. (R,I)),i) by A18, FINSEQ_1:13; :: thesis: verum