let K be Ring; :: thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B holds
(B + C) * A = (B * A) + (C * A)
let A, B, C be Matrix of K; :: thesis: ( len B = len C & width B = width C & len A = width B implies (B + C) * A = (B * A) + (C * A) )
assume that
A1: len B = len C and
A2: width B = width C and
A3: len A = width B ; :: thesis: (B + C) * A = (B * A) + (C * A)
set LHS = (B + C) * A;
set RHS = (B * A) + (C * A);
A4: ( len ((B + C) * A) = len ((B * A) + (C * A)) & len ((B + C) * A) = len B )

proof

width (B + C) = len A by A3, MATRIX_3:def 3;
then A5: len ((B + C) * A) = len (B + C) by MATRIX_3:def 4
.= len B by MATRIX_3:def 3 ;
( len (C * A) = len B & len (B * A) = len B ) by A1, A2, A3, MATRIX_3:def 4;
then len ((B * A) + (C * A)) = len B by MATRIX_3:def 3;
hence ( len ((B + C) * A) = len ((B * A) + (C * A)) & len ((B + C) * A) = len B ) by A5; :: thesis: verum

end;

per cases ( len B = 0 or len B > 0 ) by NAT_1:3;

suppose len B = 0 ; :: thesis: (B + C) * A = (B * A) + (C * A)

hence (B + C) * A = (B * A) + (C * A) by A4, CARD_2:64; :: thesis: verum

end;

suppose len B > 0 ; :: thesis: (B + C) * A = (B * A) + (C * A)

hence (B + C) * A = (B * A) + (C * A) by A1, A2, A3, Lm2; :: thesis: verum

end;

end;