let K be Field; :: thesis: for b being Element of K
for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
b * (M1 + M2) = (b * M1) + (b * M2)
let b be Element of K; :: thesis: for M1, M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds
b * (M1 + M2) = (b * M1) + (b * M2)
let M1, M2 be Matrix of K; :: thesis: ( len M1 = len M2 & width M1 = width M2 implies b * (M1 + M2) = (b * M1) + (b * M2) )
A1: ( len (b * (M1 + M2)) = len (M1 + M2) & width (b * (M1 + M2)) = width (M1 + M2) ) by MATRIX_3:def 5;
A2: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by MATRIX_3:def 3;
A3: ( len (b * M1) = len M1 & width (b * M1) = width M1 ) by MATRIX_3:def 5;
assume A4: ( len M1 = len M2 & width M1 = width M2 ) ; :: thesis: b * (M1 + M2) = (b * M1) + (b * M2)
A5: for i, j being Nat st [i,j] in Indices (b * (M1 + M2)) holds
(b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (b * (M1 + M2)) implies (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j) )
assume A6: [i,j] in Indices (b * (M1 + M2)) ; :: thesis: (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j)
A7: Indices M2 = Indices M1 by A4, MATRIX_4:55;
A8: Indices (b * (M1 + M2)) = Indices (M1 + M2) by A1, MATRIX_4:55;
A9: Indices (M1 + M2) = Indices M1 by A2, MATRIX_4:55;
Indices (b * M1) = Indices M1 by A3, MATRIX_4:55;
then ((b * M1) + (b * M2)) * (i,j) = ((b * M1) * (i,j)) + ((b * M2) * (i,j)) by A6, A8, A9, MATRIX_3:def 3
.= (b * (M1 * (i,j))) + ((b * M2) * (i,j)) by A6, A8, A9, MATRIX_3:def 5
.= (b * (M1 * (i,j))) + (b * (M2 * (i,j))) by A6, A8, A9, A7, MATRIX_3:def 5
.= b * ((M1 * (i,j)) + (M2 * (i,j))) by VECTSP_1:def 7 ;
then ((b * M1) + (b * M2)) * (i,j) = b * ((M1 + M2) * (i,j)) by A6, A8, A9, MATRIX_3:def 3
.= (b * (M1 + M2)) * (i,j) by A6, A8, MATRIX_3:def 5 ;
hence (b * (M1 + M2)) * (i,j) = ((b * M1) + (b * M2)) * (i,j) ; :: thesis: verum

end;

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