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_1: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_1: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_1:def 8;
then A13: len (Line A,i) = len (Col B,j) by MATRIX_1:def 9;
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 FINSEQ_1:def 18
.= len (mlt q1,q3) by FINSEQ_1:def 18
.= 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:3;
len (Line A,i) = len C by A1, A3, MATRIX_1:def 8;
then A16: len (Line A,i) = len (Col C,j) by MATRIX_1:def 9;
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 10
.= (Sum (mlt (Line A,i),(Col B,j))) + (Sum (mlt (Line A,i),(Col C,j))) by FVSUM_1:def 10 ;
j in Seg (width B) by A8, A17, ZFMISC_1:106;
then A19: [1,j] in Indices B by A15, ZFMISC_1:106;
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 10
.= 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_1:21; :: thesis: verum