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

end;

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