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 A2, MATRIX_4:55;
Indices (a * M) = Indices M by A1, MATRIX_4:55;
then ((a * M) + (b * M)) * (i,j) = ((a * M) * (i,j)) + ((b * M) * (i,j)) by A4, A5, MATRIX_3:def 3
.= (a * (M * (i,j))) + ((b * M) * (i,j)) by A4, A5, MATRIX_3:def 5
.= (a * (M * (i,j))) + (b * (M * (i,j))) by A4, A5, MATRIX_3:def 5
.= (a + b) * (M * (i,j)) by VECTSP_1:def 7 ;
hence ((a + b) * M) * (i,j) = ((a * M) + (b * M)) * (i,j) by A4, A5, MATRIX_3:def 5; :: 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 A2, A1, A3, MATRIX_0:21; :: thesis: verum