let R be Ring; :: thesis: for n, i, j being Nat
for r being Element of R
for A being Matrix of n,R holds
( A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A iff A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A )
let n be Nat; :: thesis: for i, j being Nat
for r being Element of R
for A being Matrix of n,R holds
( A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A iff A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A )
let i, j be Nat; :: thesis: for r being Element of R
for A being Matrix of n,R holds
( A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A iff A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A )
let r be Element of R; :: thesis: for A being Matrix of n,R holds
( A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A iff A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A )
let A be Matrix of n,R; :: thesis: ( A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A iff A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A )

per cases ( n > 0 or n = 0 ) ;

suppose A1: n > 0 ; :: thesis: ( A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A iff A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A )

A2: ( len (1. (R,n)) = len (r * (canMat (i,j,n,R))) & width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & width A = len (1. (R,n)) & len A > 0 & len (1. (R,n)) > 0 )

proof

thus len (1. (R,n)) = n by MATRIX_0:24
.= len (r * (canMat (i,j,n,R))) by MATRIX_0:24 ; :: thesis: ( width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & width A = len (1. (R,n)) & len A > 0 & len (1. (R,n)) > 0 )
thus width (1. (R,n)) = n by MATRIX_0:24
.= width (r * (canMat (i,j,n,R))) by MATRIX_0:24 ; :: thesis: ( width A = len (1. (R,n)) & len A > 0 & len (1. (R,n)) > 0 )
thus width A = n by MATRIX_0:24
.= len (1. (R,n)) by MATRIX_0:24 ; :: thesis: ( len A > 0 & len (1. (R,n)) > 0 )
thus len A > 0 by A1, MATRIX_0:24; :: thesis: len (1. (R,n)) > 0
thus len (1. (R,n)) > 0 by A1, MATRIX_0:24; :: thesis: verum

end;

A3: ( len (1. (R,n)) = len (r * (canMat (i,j,n,R))) & width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & len A = width (1. (R,n)) & len (1. (R,n)) > 0 & len A > 0 )

proof

thus len (1. (R,n)) = len (r * (canMat (i,j,n,R))) by A2; :: thesis: ( width (1. (R,n)) = width (r * (canMat (i,j,n,R))) & len A = width (1. (R,n)) & len (1. (R,n)) > 0 & len A > 0 )
thus width (1. (R,n)) = width (r * (canMat (i,j,n,R))) by A2; :: thesis: ( len A = width (1. (R,n)) & len (1. (R,n)) > 0 & len A > 0 )
thus len A = n by MATRIX_0:24
.= width (1. (R,n)) by MATRIX_0:24 ; :: thesis: ( len (1. (R,n)) > 0 & len A > 0 )
thus len (1. (R,n)) > 0 by A2; :: thesis: len A > 0
thus len A > 0 by A2; :: thesis: verum

end;

hereby :: thesis: ( A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A implies A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A )

assume A4: A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A ; :: thesis: A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A
A5: ( len (A * (r * (canMat (i,j,n,R)))) = len ((r * (canMat (i,j,n,R))) * A) & len ((r * (canMat (i,j,n,R))) * A) = len A & width (A * (r * (canMat (i,j,n,R)))) = width ((r * (canMat (i,j,n,R))) * A) & width ((r * (canMat (i,j,n,R))) * A) = width A )

proof

thus len (A * (r * (canMat (i,j,n,R)))) = n by MATRIX_0:24
.= len ((r * (canMat (i,j,n,R))) * A) by MATRIX_0:24 ; :: thesis: ( len ((r * (canMat (i,j,n,R))) * A) = len A & width (A * (r * (canMat (i,j,n,R)))) = width ((r * (canMat (i,j,n,R))) * A) & width ((r * (canMat (i,j,n,R))) * A) = width A )
thus len ((r * (canMat (i,j,n,R))) * A) = n by MATRIX_0:24
.= len A by MATRIX_0:24 ; :: thesis: ( width (A * (r * (canMat (i,j,n,R)))) = width ((r * (canMat (i,j,n,R))) * A) & width ((r * (canMat (i,j,n,R))) * A) = width A )
thus width (A * (r * (canMat (i,j,n,R)))) = n by MATRIX_0:24
.= width ((r * (canMat (i,j,n,R))) * A) by MATRIX_0:24 ; :: thesis: width ((r * (canMat (i,j,n,R))) * A) = width A
len A = n by MATRIX_0:24
.= width (r * (canMat (i,j,n,R))) by MATRIX_0:24 ;
hence width ((r * (canMat (i,j,n,R))) * A) = width A by MATRIX_3:def 4; :: thesis: verum

end;

A6: A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = (A * (1. (R,n))) + (A * (r * (canMat (i,j,n,R)))) by A2, MATRIX_4:62
.= A + (A * (r * (canMat (i,j,n,R)))) by MATRIX_3:19 ;
((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A = ((1. (R,n)) * A) + ((r * (canMat (i,j,n,R))) * A) by A3, MATRIX_4:63
.= A + ((r * (canMat (i,j,n,R))) * A) by MATRIX_3:18 ;
then A + ((r * (canMat (i,j,n,R))) * A) = (A * (r * (canMat (i,j,n,R)))) + A by A4, A6, MATRIX_1:3;
then ((r * (canMat (i,j,n,R))) * A) + A = (A * (r * (canMat (i,j,n,R)))) + A by MATRIX_1:3;
hence A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A by A5, MATRIX_4:4; :: thesis: verum

end;

assume A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A ; :: thesis: A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A
then A + (A * (r * (canMat (i,j,n,R)))) = ((1. (R,n)) * A) + ((r * (canMat (i,j,n,R))) * A) by MATRIX_3:18;
then (A * (1. (R,n))) + (A * (r * (canMat (i,j,n,R)))) = ((1. (R,n)) * A) + ((r * (canMat (i,j,n,R))) * A) by MATRIX_3:19
.= ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A by A3, MATRIX_4:63 ;
hence ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A = A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) by A2, MATRIX_4:62; :: thesis: verum

end;

suppose n = 0 ; :: thesis: ( A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A iff A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A )

hence ( A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A iff A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A ) by MATRIX_0:45; :: thesis: verum

end;

end;