let R be Ring; :: thesis: for n being Nat
for x, y being Element of R holds (x * (1. (R,n))) * y = (x * y) * (1. (R,n))
let n be Nat; :: thesis: for x, y being Element of R holds (x * (1. (R,n))) * y = (x * y) * (1. (R,n))
let x, y be Element of R; :: thesis: (x * (1. (R,n))) * y = (x * y) * (1. (R,n))
set LHS = (x * (1. (R,n))) * y;
set RHS = (x * y) * (1. (R,n));
A1: ( len ((x * (1. (R,n))) * y) = len ((x * y) * (1. (R,n))) & width ((x * (1. (R,n))) * y) = width ((x * y) * (1. (R,n))) )

proof

thus len ((x * (1. (R,n))) * y) = len (x * (1. (R,n))) by MATRIX_3:def 6
.= len (1. (R,n)) by MATRIX_3:def 5
.= len ((x * y) * (1. (R,n))) by MATRIX_3:def 5 ; :: thesis: width ((x * (1. (R,n))) * y) = width ((x * y) * (1. (R,n)))
thus width ((x * (1. (R,n))) * y) = width (x * (1. (R,n))) by MATRIX_3:def 6
.= width (1. (R,n)) by MATRIX_3:def 5
.= width ((x * y) * (1. (R,n))) by MATRIX_3:def 5 ; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices ((x * (1. (R,n))) * y) holds
((x * (1. (R,n))) * y) * (i,j) = ((x * y) * (1. (R,n))) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((x * (1. (R,n))) * y) implies ((x * (1. (R,n))) * y) * (i,j) = ((x * y) * (1. (R,n))) * (i,j) )
assume A2: [i,j] in Indices ((x * (1. (R,n))) * y) ; :: thesis: ((x * (1. (R,n))) * y) * (i,j) = ((x * y) * (1. (R,n))) * (i,j)
A3: ( [i,j] in Indices (x * (1. (R,n))) & [i,j] in Indices (1. (R,n)) )

proof

A4: Indices ((x * (1. (R,n))) * y) = [:(dom ((x * (1. (R,n))) * y)),(Seg (width ((x * (1. (R,n))) * y))):] by MATRIX_0:def 4
.= [:(Seg (len ((x * (1. (R,n))) * y))),(Seg (width ((x * (1. (R,n))) * y))):] by FINSEQ_1:def 3
.= [:(Seg (len (x * (1. (R,n))))),(Seg (width ((x * (1. (R,n))) * y))):] by MATRIX_3:def 6
.= [:(Seg (len (x * (1. (R,n))))),(Seg (width (x * (1. (R,n))))):] by MATRIX_3:def 6 ;
then Indices ((x * (1. (R,n))) * y) = [:(dom (x * (1. (R,n)))),(Seg (width (x * (1. (R,n))))):] by FINSEQ_1:def 3;
hence [i,j] in Indices (x * (1. (R,n))) by A2, MATRIX_0:def 4; :: thesis: [i,j] in Indices (1. (R,n))
Indices ((x * (1. (R,n))) * y) = [:(Seg (len (1. (R,n)))),(Seg (width (x * (1. (R,n))))):] by A4, MATRIX_3:def 5
.= [:(Seg (len (1. (R,n)))),(Seg (width (1. (R,n)))):] by MATRIX_3:def 5
.= [:(dom (1. (R,n))),(Seg (width (1. (R,n)))):] by FINSEQ_1:def 3
.= Indices (1. (R,n)) by MATRIX_0:def 4 ;
hence [i,j] in Indices (1. (R,n)) by A2; :: thesis: verum

end;

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

suppose A5: i = j ; :: thesis: ((x * (1. (R,n))) * y) * (i,j) = ((x * y) * (1. (R,n))) * (i,j)

thus ((x * (1. (R,n))) * y) * (i,j) = ((x * (1. (R,n))) * (i,j)) * y by A3, MATRIX_3:def 6
.= (x * ((1. (R,n)) * (i,j))) * y by A3, MATRIX_3:def 5
.= (x * (1. R)) * y by A3, A5, MATRIX_1:def 3
.= (x * y) * (1. R)
.= (x * y) * ((1. (R,n)) * (i,j)) by A3, A5, MATRIX_1:def 3
.= ((x * y) * (1. (R,n))) * (i,j) by A3, MATRIX_3:def 5 ; :: thesis: verum

end;

suppose A6: i <> j ; :: thesis: ((x * (1. (R,n))) * y) * (i,j) = ((x * y) * (1. (R,n))) * (i,j)

thus ((x * (1. (R,n))) * y) * (i,j) = ((x * (1. (R,n))) * (i,j)) * y by A3, MATRIX_3:def 6
.= (x * ((1. (R,n)) * (i,j))) * y by A3, MATRIX_3:def 5
.= (x * (0. R)) * y by A3, A6, MATRIX_1:def 3
.= (x * y) * (0. R)
.= (x * y) * ((1. (R,n)) * (i,j)) by A3, A6, MATRIX_1:def 3
.= ((x * y) * (1. (R,n))) * (i,j) by A3, MATRIX_3:def 5 ; :: thesis: verum

end;

end;

end;

hence (x * (1. (R,n))) * y = (x * y) * (1. (R,n)) by A1, MATRIX_0:21; :: thesis: verum