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 A3, MATRIX_3:def 4;
A8: ( width (B + C) = width B & width (A * (B + C)) = width (B + C) ) by A3, A6, MATRIX_3:def 3, MATRIX_3:def 4;
then reconsider M1 = A * (B + C) as Matrix of len A, width B,K by A4, A7, MATRIX_0:20;
A9: ( len (A * B) = len A & width (A * B) = width B ) by A3, MATRIX_3:def 4;
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 A4, A9, MATRIX_0:20;
( len (A * C) = len A & width (A * C) = width C ) by A1, A3, MATRIX_3:def 4;
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 A3, MATRIX_0:def 7;
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 A5, FINSEQ_1:def 3, NAT_1:13;
then A15: 1 in dom B by FINSEQ_1:1;
len (Line (A,i)) = len C by A1, A3, MATRIX_0:def 7;
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 A10, MATRIX_3:def 3
.= ((Line (A,i)) "*" (Col (B,j))) + ((A * C) * (i,j)) by A3, A10, A17, MATRIX_3:def 4
.= ((Line (A,i)) "*" (Col (B,j))) + ((Line (A,i)) "*" (Col (C,j))) by A1, A3, A12, A17, MATRIX_3:def 4
.= ((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 (width B) by A8, A17, ZFMISC_1:87;
then A19: [1,j] in Indices B by A15, ZFMISC_1:87;
M1 * (i,j) = (Line (A,i)) "*" (Col ((B + C),j)) by A3, A6, A17, MATRIX_3:def 4
.= 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 A1, A19, Th60
.= Sum ((mlt ((Line (A,i)),(Col (B,j)))) + (mlt ((Line (A,i)),(Col (C,j))))) by A13, A16, Th57
.= (Sum (mlt ((Line (A,i)),(Col (B,j))))) + (Sum (mlt ((Line (A,i)),(Col (C,j))))) by A14, Th61 ;
hence M1 * (i,j) = M2 * (i,j) by A18; :: thesis: verum

end;

hence A * (B + C) = (A * B) + (A * C) by A7, A8, A9, A11, MATRIX_0:21; :: thesis: verum