let R be Ring; :: thesis: for n being Nat
for r being Element of R
for i, j being Nat holds (canMat (i,j,n,R)) * r = r * (canMat (i,j,n,R))
let n be Nat; :: thesis: for r being Element of R
for i, j being Nat holds (canMat (i,j,n,R)) * r = r * (canMat (i,j,n,R))
let r be Element of R; :: thesis: for i, j being Nat holds (canMat (i,j,n,R)) * r = r * (canMat (i,j,n,R))
let i, j be Nat; :: thesis: (canMat (i,j,n,R)) * r = r * (canMat (i,j,n,R))
A1: len ((canMat (i,j,n,R)) * r) = len (canMat (i,j,n,R)) by MATRIX_3:def 6
.= len (r * (canMat (i,j,n,R))) by MATRIX_3:def 5 ;
A2: width ((canMat (i,j,n,R)) * r) = width (canMat (i,j,n,R)) by MATRIX_3:def 6
.= width (r * (canMat (i,j,n,R))) by MATRIX_3:def 5 ;
for i2, j2 being Nat st [i2,j2] in Indices ((canMat (i,j,n,R)) * r) holds
((canMat (i,j,n,R)) * r) * (i2,j2) = (r * (canMat (i,j,n,R))) * (i2,j2)

proof

let i2, j2 be Nat; :: thesis: ( [i2,j2] in Indices ((canMat (i,j,n,R)) * r) implies ((canMat (i,j,n,R)) * r) * (i2,j2) = (r * (canMat (i,j,n,R))) * (i2,j2) )
assume A3: [i2,j2] in Indices ((canMat (i,j,n,R)) * r) ; :: thesis: ((canMat (i,j,n,R)) * r) * (i2,j2) = (r * (canMat (i,j,n,R))) * (i2,j2)
A4: [i2,j2] in Indices (canMat (i,j,n,R))

proof

A5: dom ((canMat (i,j,n,R)) * r) = Seg (len ((canMat (i,j,n,R)) * r)) by FINSEQ_1:def 3
.= Seg (len (canMat (i,j,n,R))) by MATRIX_3:def 6
.= dom (canMat (i,j,n,R)) by FINSEQ_1:def 3 ;
Seg (width ((canMat (i,j,n,R)) * r)) = Seg (width (canMat (i,j,n,R))) by MATRIX_3:def 6;
then [:(dom ((canMat (i,j,n,R)) * r)),(Seg (width ((canMat (i,j,n,R)) * r))):] = Indices (canMat (i,j,n,R)) by A5, MATRIX_0:def 4;
hence [i2,j2] in Indices (canMat (i,j,n,R)) by A3, MATRIX_0:def 4; :: thesis: verum

end;

per cases ( [i,j] = [i2,j2] or [i,j] <> [i2,j2] ) ;

suppose A6: [i,j] = [i2,j2] ; :: thesis: ((canMat (i,j,n,R)) * r) * (i2,j2) = (r * (canMat (i,j,n,R))) * (i2,j2)

thus ((canMat (i,j,n,R)) * r) * (i2,j2) = ((canMat (i,j,n,R)) * (i2,j2)) * r by A4, MATRIX_3:def 6
.= (1. R) * r by A4, A6, Def1
.= r * (1. R)
.= r * ((canMat (i,j,n,R)) * (i2,j2)) by A4, A6, Def1
.= (r * (canMat (i,j,n,R))) * (i2,j2) by A4, MATRIX_3:def 5 ; :: thesis: verum

end;

suppose A7: [i,j] <> [i2,j2] ; :: thesis: ((canMat (i,j,n,R)) * r) * (i2,j2) = (r * (canMat (i,j,n,R))) * (i2,j2)

thus ((canMat (i,j,n,R)) * r) * (i2,j2) = ((canMat (i,j,n,R)) * (i2,j2)) * r by A4, MATRIX_3:def 6
.= (0. R) * r by A4, A7, Def1
.= r * (0. R)
.= r * ((canMat (i,j,n,R)) * (i2,j2)) by A4, A7, Def1
.= (r * (canMat (i,j,n,R))) * (i2,j2) by A4, MATRIX_3:def 5 ; :: thesis: verum

end;

end;

end;

hence (canMat (i,j,n,R)) * r = r * (canMat (i,j,n,R)) by A1, A2, MATRIX_0:21; :: thesis: verum