let R be Ring; :: thesis: for n, i, j being Nat st [i,j] in Indices (canMat (i,j,n,R)) holds
for A being Matrix of n,R
for i2, j2 being Nat st [i2,j2] in Indices A holds
( ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) & ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R ) )
let n be Nat; :: thesis: for i, j being Nat st [i,j] in Indices (canMat (i,j,n,R)) holds
for A being Matrix of n,R
for i2, j2 being Nat st [i2,j2] in Indices A holds
( ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) & ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R ) )
let i, j be Nat; :: thesis: ( [i,j] in Indices (canMat (i,j,n,R)) implies for A being Matrix of n,R
for i2, j2 being Nat st [i2,j2] in Indices A holds
( ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) & ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R ) ) )
assume [i,j] in Indices (canMat (i,j,n,R)) ; :: thesis: for A being Matrix of n,R
for i2, j2 being Nat st [i2,j2] in Indices A holds
( ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) & ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R ) )
then A6: [i,j] in [:(Seg n),(Seg n):] by MATRIX_0:24;
let A be Matrix of n,R; :: thesis: for i2, j2 being Nat st [i2,j2] in Indices A holds
( ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) & ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R ) )
let i2, j2 be Nat; :: thesis: ( [i2,j2] in Indices A implies ( ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) & ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R ) ) )
assume A2: [i2,j2] in Indices A ; :: thesis: ( ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) & ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R ) )
A3: [i,j2] in Indices (canMat (i,j,n,R))

proof

A4: i in Seg n by A6, ZFMISC_1:87;
[i2,j2] in [:(Seg n),(Seg n):] by A2, MATRIX_0:24;
then j2 in Seg n by ZFMISC_1:87;
then [i,j2] in [:(Seg n),(Seg n):] by A4, ZFMISC_1:87;
hence [i,j2] in Indices (canMat (i,j,n,R)) by MATRIX_0:24; :: thesis: verum

end;

A5: ( i in dom A & i in dom (1. (R,n)) )

proof

dom A = Seg (len A) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24 ;
hence i in dom A by A6, ZFMISC_1:87; :: thesis: i in dom (1. (R,n))
dom (1. (R,n)) = Seg (len (1. (R,n))) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24 ;
hence i in dom (1. (R,n)) by A6, ZFMISC_1:87; :: thesis: verum

end;

A7: width A = n by MATRIX_0:24
.= len (canMat (i,j,n,R)) by MATRIX_0:25 ;
A8: [i2,j2] in Indices (A * (canMat (i,j,n,R)))

proof

Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices (A * (canMat (i,j,n,R))) by MATRIX_0:24 ;
hence [i2,j2] in Indices (A * (canMat (i,j,n,R))) by A2; :: thesis: verum

end;

thus ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) :: thesis: ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R )

proof

assume A9: j = j2 ; :: thesis: (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i)
thus (A * (canMat (i,j,n,R))) * (i2,j2) = (Line (A,i2)) "*" (Col ((canMat (i,j,n,R)),j2)) by A7, A8, MATRIX_3:def 4
.= (Line (A,i2)) "*" (Col ((1. (R,n)),i)) by A3, A9, Th45
.= A * (i2,i) by A5, Th23 ; :: thesis: verum

end;

assume A10: j <> j2 ; :: thesis: (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R
A11: dom (0. (R,n)) = Seg (len (0. (R,n))) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24
.= Seg (len (1. (R,n))) by MATRIX_0:24
.= dom (1. (R,n)) by FINSEQ_1:def 3 ;
thus (A * (canMat (i,j,n,R))) * (i2,j2) = (Line (A,i2)) "*" (Col ((canMat (i,j,n,R)),j2)) by A7, A8, MATRIX_3:def 4
.= (Line (A,i2)) "*" (Col ((0. (R,n)),i)) by A3, A10, Th45
.= 0. R by A5, A11, Th20 ; :: thesis: verum