let L be Field; :: thesis: for m, n, k being Element of NAT st m > 0 & n > 0 holds
for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)
let m, n, k be Element of NAT ; :: thesis: ( m > 0 & n > 0 implies for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2) )
assume that
A1: m > 0 and
A2: n > 0 ; :: thesis: for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)
let M1 be Matrix of m,n,L; :: thesis: for M2 being Matrix of n,k,L holds ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)
let M2 be Matrix of n,k,L; :: thesis: ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)
A3: width M1 = n by A1, MATRIX_1:24
.= len M2 by A2, MATRIX_1:24 ;
A4: width ((emb m,L) * M1) = width M1 by MATRIX_3:def 5
.= n by A1, MATRIX_1:24
.= len M2 by A2, MATRIX_1:24 ;
A5: for i, j being Nat st [i,j] in Indices (((emb m,L) * M1) * M2) holds
(((emb m,L) * M1) * M2) * i,j = ((emb m,L) * (M1 * M2)) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (((emb m,L) * M1) * M2) implies (((emb m,L) * M1) * M2) * i,j = ((emb m,L) * (M1 * M2)) * i,j )
A6: len M1 = len (M1 * M2) by A3, MATRIX_3:def 4;
len (((emb m,L) * M1) * M2) = len ((emb m,L) * M1) by A4, MATRIX_3:def 4
.= len M1 by MATRIX_3:def 5 ;
then A7: dom (((emb m,L) * M1) * M2) = Seg (len M1) by FINSEQ_1:def 3
.= dom (M1 * M2) by A6, FINSEQ_1:def 3 ;
Seg (len ((emb m,L) * (Line M1,i))) = dom ((emb m,L) * (Line M1,i)) by FINSEQ_1:def 3
.= dom (Line M1,i) by POLYNOM1:def 2
.= Seg (len (Line M1,i)) by FINSEQ_1:def 3 ;
then A8: len ((emb m,L) * (Line M1,i)) = len (Line M1,i) by FINSEQ_1:8
.= width M1 by MATRIX_1:def 8 ;
A9: len (Line M1,i) = len M2 by A3, MATRIX_1:def 8
.= len (Col M2,j) by MATRIX_1:def 9 ;
assume A10: [i,j] in Indices (((emb m,L) * M1) * M2) ; :: thesis: (((emb m,L) * M1) * M2) * i,j = ((emb m,L) * (M1 * M2)) * i,j
then A11: (((emb m,L) * M1) * M2) * i,j = (Line ((emb m,L) * M1),i) "*" (Col M2,j) by A4, MATRIX_3:def 4
.= Sum (mlt (Line ((emb m,L) * M1),i),(Col M2,j)) by FVSUM_1:def 10 ;
len (Line ((emb m,L) * M1),i) = width ((emb m,L) * M1) by MATRIX_1:def 8
.= width M1 by MATRIX_3:def 5 ;
then dom (Line ((emb m,L) * M1),i) = Seg (width M1) by FINSEQ_1:def 3;
then A12: dom (Line ((emb m,L) * M1),i) = dom ((emb m,L) * (Line M1,i)) by A8, FINSEQ_1:def 3;
for k being Nat st k in dom (Line ((emb m,L) * M1),i) holds
(Line ((emb m,L) * M1),i) . k = ((emb m,L) * (Line M1,i)) . k

proof

len (M1 * M2) = len M1 by A3, MATRIX_3:def 4
.= m by A1, MATRIX_1:24 ;
then A13: dom (M1 * M2) = Seg m by FINSEQ_1:def 3;
A14: ( Indices M1 = [:(Seg m),(Seg n):] & i in dom (M1 * M2) ) by A1, A10, A7, MATRIX_1:24, ZFMISC_1:106;
let k be Nat; :: thesis: ( k in dom (Line ((emb m,L) * M1),i) implies (Line ((emb m,L) * M1),i) . k = ((emb m,L) * (Line M1,i)) . k )
assume A15: k in dom (Line ((emb m,L) * M1),i) ; :: thesis: (Line ((emb m,L) * M1),i) . k = ((emb m,L) * (Line M1,i)) . k
A16: len (Line ((emb m,L) * M1),i) = width ((emb m,L) * M1) by MATRIX_1:def 8
.= width M1 by MATRIX_3:def 5 ;
then A17: k in Seg (width M1) by A15, FINSEQ_1:def 3;
len (Line M1,i) = width M1 by MATRIX_1:def 8;
then k in dom (Line M1,i) by A17, FINSEQ_1:def 3;
then (Line M1,i) . k = (Line M1,i) /. k by PARTFUN1:def 8;
then reconsider a = (Line M1,i) . k as Element of L ;
A18: a = M1 * i,k by A17, MATRIX_1:def 8;
k in Seg n by A1, A17, MATRIX_1:24;
then [i,k] in Indices M1 by A14, A13, ZFMISC_1:106;
then A19: (emb m,L) * a = ((emb m,L) * M1) * i,k by A18, MATRIX_3:def 5;
dom (Line ((emb m,L) * M1),i) = Seg (width M1) by A16, FINSEQ_1:def 3;
then A20: k in Seg (width ((emb m,L) * M1)) by A15, MATRIX_3:def 5;
((emb m,L) * (Line M1,i)) . k = (emb m,L) * a by A12, A15, FVSUM_1:62;
hence (Line ((emb m,L) * M1),i) . k = ((emb m,L) * (Line M1,i)) . k by A20, A19, MATRIX_1:def 8; :: thesis: verum

end;

then A21: Line ((emb m,L) * M1),i = (emb m,L) * (Line M1,i) by A12, FINSEQ_1:17;
Seg (len ((emb m,L) * (Line M1,i))) = dom ((emb m,L) * (Line M1,i)) by FINSEQ_1:def 3
.= dom (Line M1,i) by POLYNOM1:def 2
.= Seg (len (Line M1,i)) by FINSEQ_1:def 3 ;
then A22: len ((emb m,L) * (Line M1,i)) = len (Line M1,i) by FINSEQ_1:8
.= len M2 by A3, MATRIX_1:def 8
.= len (Col M2,j) by MATRIX_1:def 9 ;
A23: dom ((emb m,L) * (Line M1,i)) = Seg (len ((emb m,L) * (Line M1,i))) by FINSEQ_1:def 3
.= Seg (len (mlt ((emb m,L) * (Line M1,i)),(Col M2,j))) by A22, MATRIX_3:8
.= dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) by FINSEQ_1:def 3 ;
A24: dom ((emb m,L) * (Line M1,i)) = dom (Line M1,i) by POLYNOM1:def 2
.= Seg (len (Line M1,i)) by FINSEQ_1:def 3
.= Seg (len (mlt (Line M1,i),(Col M2,j))) by A9, MATRIX_3:8
.= dom (mlt (Line M1,i),(Col M2,j)) by FINSEQ_1:def 3 ;
then A25: dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) = dom ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) by A23, POLYNOM1:def 2;
for k being Nat st k in dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) holds
(mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) . k = ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k

proof

A26: len (Line M1,i) = len M2 by A3, MATRIX_1:def 8
.= len (Col M2,j) by MATRIX_1:def 9 ;
A27: len (Line M1,i) = width M1 by MATRIX_1:def 8;
let k be Nat; :: thesis: ( k in dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) implies (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) . k = ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k )
assume A28: k in dom (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) ; :: thesis: (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) . k = ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k
dom (Line M1,i) = Seg (len (Line M1,i)) by FINSEQ_1:def 3
.= Seg (len (mlt (Line M1,i),(Col M2,j))) by A26, MATRIX_3:8
.= dom (mlt (Line M1,i),(Col M2,j)) by FINSEQ_1:def 3 ;
then A29: k in Seg (width M1) by A23, A24, A28, A27, FINSEQ_1:def 3;
then k in dom M2 by A3, FINSEQ_1:def 3;
then A30: (Col M2,j) . k = M2 * k,j by MATRIX_1:def 9;
(Line M1,i) . k = M1 * i,k by A29, MATRIX_1:def 8;
then reconsider c = (Col M2,j) . k, d = (Line M1,i) . k as Element of L by A30;
(mlt (Line M1,i),(Col M2,j)) . k = c * d by A23, A24, A28, FVSUM_1:73;
then reconsider a = (mlt (Line M1,i),(Col M2,j)) . k as Element of L ;
A31: ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k = (emb m,L) * a by A25, A28, FVSUM_1:62;
((emb m,L) * (Line M1,i)) . k = (emb m,L) * d by A23, A28, FVSUM_1:62;
then reconsider b = ((emb m,L) * (Line M1,i)) . k as Element of L ;
b * c = ((emb m,L) * d) * c by A23, A28, FVSUM_1:62
.= (emb m,L) * (d * c) by GROUP_1:def 4
.= (emb m,L) * a by A23, A24, A28, FVSUM_1:73 ;
hence (mlt ((emb m,L) * (Line M1,i)),(Col M2,j)) . k = ((emb m,L) * (mlt (Line M1,i),(Col M2,j))) . k by A28, A31, FVSUM_1:73; :: thesis: verum

end;

then A32: (emb m,L) * (mlt (Line M1,i),(Col M2,j)) = mlt (Line ((emb m,L) * M1),i),(Col M2,j) by A21, A25, FINSEQ_1:17;
Seg (width (((emb m,L) * M1) * M2)) = Seg (width M2) by A4, MATRIX_3:def 4
.= Seg (width (M1 * M2)) by A3, MATRIX_3:def 4 ;
then A33: [i,j] in Indices (M1 * M2) by A10, A7;
then ((emb m,L) * (M1 * M2)) * i,j = (emb m,L) * ((M1 * M2) * i,j) by MATRIX_3:def 5
.= (emb m,L) * ((Line M1,i) "*" (Col M2,j)) by A3, A33, MATRIX_3:def 4
.= (emb m,L) * (Sum (mlt (Line M1,i),(Col M2,j))) by FVSUM_1:def 10 ;
hence (((emb m,L) * M1) * M2) * i,j = ((emb m,L) * (M1 * M2)) * i,j by A11, A32, FVSUM_1:92; :: thesis: verum

end;

A34: len ((emb m,L) * (M1 * M2)) = len (M1 * M2) by MATRIX_3:def 5
.= len M1 by A3, MATRIX_3:def 4 ;
width ((emb m,L) * (M1 * M2)) = width (M1 * M2) by MATRIX_3:def 5
.= width M2 by A3, MATRIX_3:def 4 ;
then A35: width (((emb m,L) * M1) * M2) = width ((emb m,L) * (M1 * M2)) by A4, MATRIX_3:def 4;
len (((emb m,L) * M1) * M2) = len ((emb m,L) * M1) by A4, MATRIX_3:def 4
.= len M1 by MATRIX_3:def 5 ;
hence ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2) by A34, A35, A5, MATRIX_1:21; :: thesis: verum