let R be Ring; :: thesis:
let n be Nat; :: thesis:
let i, j be Nat; :: thesis:
assume A1: [i,j] in Indices (canMat (i,j,n,R)) ; :: thesis:
let A be Matrix of n,R; :: thesis:
let i2, j2 be Nat; :: thesis:
assume A2: [i2,j2] in Indices A ; :: thesis:
A3: Indices ((canMat (i,j,n,R)) * A) = [:(Seg n),(Seg n):] by MATRIX_0:24
.= Indices A by MATRIX_0:24 ;
A4: [i2,j] in Indices (canMat (i,j,n,R))

proof

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

end;

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

proof

assume A6: i = i2 ; :: thesis:
A7: ( j in dom (1. (R,n)) & j in dom A )

proof

A8: [i,j] in [:(Seg n),(Seg n):] by A1, MATRIX_0:24;
dom (1. (R,n)) = Seg (len (1. (R,n))) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24 ;
hence j in dom (1. (R,n)) by A8, ZFMISC_1:87; :: thesis:
dom A = Seg (len A) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24 ;
hence j in dom A by A8, ZFMISC_1:87; :: thesis:

end;

width (canMat (i,j,n,R)) = n by MATRIX_0:24
.= len A by MATRIX_0:24 ;
hence ((canMat (i,j,n,R)) * A) * (i2,j2) = (Line ((canMat (i,j,n,R)),i2)) "*" (Col (A,j2)) by A2, A3, MATRIX_3:def 4
.= (Line ((1. (R,n)),j)) "*" (Col (A,j2)) by A6, A4, Th44
.= A * (j,j2) by A7, Th21 ;
:: thesis:

end;

assume A9: i <> i2 ; :: thesis:
A10: j in dom (0. (R,n))

proof

A11: [i,j] in [:(Seg n),(Seg n):] by A1, MATRIX_0:24;
dom (0. (R,n)) = Seg (len (0. (R,n))) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24 ;
hence j in dom (0. (R,n)) by A11, ZFMISC_1:87; :: thesis:

end;

width (canMat (i,j,n,R)) = n by MATRIX_0:24
.= len A by MATRIX_0:24 ;
hence ((canMat (i,j,n,R)) * A) * (i2,j2) = (Line ((canMat (i,j,n,R)),i2)) "*" (Col (A,j2)) by A2, A3, MATRIX_3:def 4
.= (Line ((0. (R,n)),j)) "*" (Col (A,j2)) by A4, A9, Th44
.= 0. R by A10, Th19 ;
:: thesis: