let a, b be Real; :: thesis: for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A)
let A be Matrix of REAL; :: thesis: (a + b) * A = (a * A) + (b * A)
A1: ( len (a * A) = len A & width (a * A) = width A ) by MATRIXR1:27;
A2: ( len ((a + b) * A) = len A & width ((a + b) * A) = width A ) by MATRIXR1:27;
A3: for i, j being Nat st [i,j] in Indices ((a + b) * A) holds
((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((a + b) * A) implies ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j) )
assume A4: [i,j] in Indices ((a + b) * A) ; :: thesis: ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j)
reconsider i0 = i, j0 = j as Nat ;
A5: Indices ((a + b) * A) = Indices A by A2, MATRIX_4:55;
Indices (a * A) = Indices A by A1, MATRIX_4:55;
then ((a * A) + (b * A)) * (i,j) = ((a * A) * (i0,j0)) + ((b * A) * (i0,j0)) by A4, A5, MATRIXR1:25
.= (a * (A * (i0,j0))) + ((b * A) * (i0,j0)) by A4, A5, MATRIXR1:29
.= (a * (A * (i0,j0))) + (b * (A * (i0,j0))) by A4, A5, MATRIXR1:29
.= (a + b) * (A * (i,j)) ;
hence ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j) by A4, A5, MATRIXR1:29; :: thesis: verum

end;

( len ((a * A) + (b * A)) = len (a * A) & width ((a * A) + (b * A)) = width (a * A) ) by MATRIX_3:def 3;
hence (a + b) * A = (a * A) + (b * A) by A2, A1, A3, MATRIX_0:21; :: thesis: verum