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

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

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

then ( len (A * (B + C)) = 0 & len ((A * B) + (A * C)) = 0 ) by A4;
hence A * (B + C) = (A * B) + (A * C) by CARD_2:64; :: thesis: verum

end;

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

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

end;

end;