let K be Field; :: thesis: for a, b being Element of K
for M being Matrix of K holds (a + b) * M = (a * M) + (b * M)

let a, b be Element of K; :: thesis: for M being Matrix of K holds (a + b) * M = (a * M) + (b * M)
let M be Matrix of K; :: thesis: (a + b) * M = (a * M) + (b * M)
A1: ( len (a * M) = len M & width (a * M) = width M ) by MATRIX_3:def 5;
A2: ( len ((a + b) * M) = len M & width ((a + b) * M) = width M ) by MATRIX_3:def 5;
A3: for i, j being Nat st [i,j] in Indices ((a + b) * M) holds
((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j)
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices ((a + b) * M) implies ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j) )
assume A4: [i,j] in Indices ((a + b) * M) ; :: thesis: ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j)
A5: Indices ((a + b) * M) = Indices M by ;
Indices (a * M) = Indices M by ;
then ((a * M) + (b * M)) * (i,j) = ((a * M) * (i,j)) + ((b * M) * (i,j)) by
.= (a * (M * (i,j))) + ((b * M) * (i,j)) by
.= (a * (M * (i,j))) + (b * (M * (i,j))) by
.= (a + b) * (M * (i,j)) by VECTSP_1:def 7 ;
hence ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j) by ; :: thesis: verum
end;
( len ((a * M) + (b * M)) = len (a * M) & width ((a * M) + (b * M)) = width (a * M) ) by MATRIX_3:def 3;
hence (a + b) * M = (a * M) + (b * M) by ; :: thesis: verum