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 ;
A8: Indices (b * (M1 + M2)) = Indices (M1 + M2) by ;
A9: Indices (M1 + M2) = Indices M1 by ;
Indices (b * M1) = Indices M1 by ;
then ((b * M1) + (b * M2)) * (i,j) = ((b * M1) * (i,j)) + ((b * M2) * (i,j)) by
.= (b * (M1 * (i,j))) + ((b * M2) * (i,j)) by
.= (b * (M1 * (i,j))) + (b * (M2 * (i,j))) by
.= 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
.= (b * (M1 + M2)) * (i,j) by ;
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 ; :: thesis: verum