let K be Field; :: thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & width A = len B & len A > 0 & len B > 0 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 & len A > 0 & len B > 0 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 and
A4: len A > 0 and
A5: len B > 0 ; :: thesis: A * (B + C) = (A * B) + (A * C)
A6: len (B + C) = len B by MATRIX_3:def 3;
then A7: len (A * (B + C)) = len A by ;
A8: ( width (B + C) = width B & width (A * (B + C)) = width (B + C) ) by ;
then reconsider M1 = A * (B + C) as Matrix of len A, width B,K by ;
A9: ( len (A * B) = len A & width (A * B) = width B ) by ;
then A10: Indices M1 = Indices (A * B) by A7, A8, Th55;
A11: ( len ((A * B) + (A * C)) = len (A * B) & width ((A * B) + (A * C)) = width (A * B) ) by MATRIX_3:def 3;
then reconsider M2 = (A * B) + (A * C) as Matrix of len A, width B,K by ;
( len (A * C) = len A & width (A * C) = width C ) by ;
then A12: Indices M1 = Indices (A * C) by A2, A7, A8, Th55;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
len (Line (A,i)) = len B by ;
then A13: len (Line (A,i)) = len (Col (B,j)) by MATRIX_0:def 8;
reconsider q1 = Line (A,i), q2 = Col (B,j), q3 = Col (C,j) as Element of (len B) -tuples_on the carrier of K by A1, A3;
A14: len (mlt ((Line (A,i)),(Col (B,j)))) = len (mlt (q1,q2))
.= len B by CARD_1:def 7
.= len (mlt (q1,q3)) by CARD_1:def 7
.= len (mlt ((Line (A,i)),(Col (C,j)))) ;
( dom B = Seg (len B) & 1 + 0 <= len B ) by ;
then A15: 1 in dom B by FINSEQ_1:1;
len (Line (A,i)) = len C by ;
then A16: len (Line (A,i)) = len (Col (C,j)) by MATRIX_0:def 8;
assume A17: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)
then A18: M2 * (i,j) = ((A * B) * (i,j)) + ((A * C) * (i,j)) by
.= ((Line (A,i)) "*" (Col (B,j))) + ((A * C) * (i,j)) by
.= ((Line (A,i)) "*" (Col (B,j))) + ((Line (A,i)) "*" (Col (C,j))) by
.= ((Line (A,i)) "*" (Col (B,j))) + (Sum (mlt ((Line (A,i)),(Col (C,j))))) by FVSUM_1:def 9
.= (Sum (mlt ((Line (A,i)),(Col (B,j))))) + (Sum (mlt ((Line (A,i)),(Col (C,j))))) by FVSUM_1:def 9 ;
j in Seg () by ;
then A19: [1,j] in Indices B by ;
M1 * (i,j) = (Line (A,i)) "*" (Col ((B + C),j)) by
.= Sum (mlt ((Line (A,i)),(Col ((B + C),j)))) by FVSUM_1:def 9
.= Sum (mlt ((Line (A,i)),((Col (B,j)) + (Col (C,j))))) by
.= Sum ((mlt ((Line (A,i)),(Col (B,j)))) + (mlt ((Line (A,i)),(Col (C,j))))) by
.= (Sum (mlt ((Line (A,i)),(Col (B,j))))) + (Sum (mlt ((Line (A,i)),(Col (C,j))))) by ;
hence M1 * (i,j) = M2 * (i,j) by A18; :: thesis: verum
end;
hence A * (B + C) = (A * B) + (A * C) by ; :: thesis: verum