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_0:23

.= len M2 by A2, MATRIX_0:23 ;

A4: width ((emb (m,L)) * M1) = width M1 by MATRIX_3:def 5

.= n by A1, MATRIX_0:23

.= len M2 by A2, MATRIX_0:23 ;

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)

.= 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_0:21; :: thesis: verum

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_0:23

.= len M2 by A2, MATRIX_0:23 ;

A4: width ((emb (m,L)) * M1) = width M1 by MATRIX_3:def 5

.= n by A1, MATRIX_0:23

.= len M2 by A2, MATRIX_0:23 ;

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

A34: len ((emb (m,L)) * (M1 * M2)) =
len (M1 * M2)
by MATRIX_3:def 5
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 1

.= 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:6

.= width M1 by MATRIX_0:def 7 ;

A9: len (Line (M1,i)) = len M2 by A3, MATRIX_0:def 7

.= len (Col (M2,j)) by MATRIX_0:def 8 ;

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 9 ;

len (Line (((emb (m,L)) * M1),i)) = width ((emb (m,L)) * M1) by MATRIX_0:def 7

.= 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

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 1

.= 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:6

.= len M2 by A3, MATRIX_0:def 7

.= len (Col (M2,j)) by MATRIX_0:def 8 ;

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:6

.= 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 1

.= Seg (len (Line (M1,i))) by FINSEQ_1:def 3

.= Seg (len (mlt ((Line (M1,i)),(Col (M2,j))))) by A9, MATRIX_3:6

.= 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 1;

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

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 9 ;

hence (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) by A11, A32, FVSUM_1:73; :: thesis: verum

end;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 1

.= 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:6

.= width M1 by MATRIX_0:def 7 ;

A9: len (Line (M1,i)) = len M2 by A3, MATRIX_0:def 7

.= len (Col (M2,j)) by MATRIX_0:def 8 ;

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 9 ;

len (Line (((emb (m,L)) * M1),i)) = width ((emb (m,L)) * M1) by MATRIX_0:def 7

.= 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

then A21:
Line (((emb (m,L)) * M1),i) = (emb (m,L)) * (Line (M1,i))
by A12, FINSEQ_1:13;
len (M1 * M2) =
len M1
by A3, MATRIX_3:def 4

.= m by A1, MATRIX_0:23 ;

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_0:23, ZFMISC_1:87;

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_0:def 7

.= 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_0:def 7;

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 6;

then reconsider a = (Line (M1,i)) . k as Element of L ;

A18: a = M1 * (i,k) by A17, MATRIX_0:def 7;

k in Seg n by A1, A17, MATRIX_0:23;

then [i,k] in Indices M1 by A14, A13, ZFMISC_1:87;

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:50;

hence (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k by A20, A19, MATRIX_0:def 7; :: thesis: verum

end;.= m by A1, MATRIX_0:23 ;

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_0:23, ZFMISC_1:87;

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_0:def 7

.= 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_0:def 7;

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 6;

then reconsider a = (Line (M1,i)) . k as Element of L ;

A18: a = M1 * (i,k) by A17, MATRIX_0:def 7;

k in Seg n by A1, A17, MATRIX_0:23;

then [i,k] in Indices M1 by A14, A13, ZFMISC_1:87;

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:50;

hence (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k by A20, A19, MATRIX_0:def 7; :: thesis: verum

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 1

.= 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:6

.= len M2 by A3, MATRIX_0:def 7

.= len (Col (M2,j)) by MATRIX_0:def 8 ;

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:6

.= 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 1

.= Seg (len (Line (M1,i))) by FINSEQ_1:def 3

.= Seg (len (mlt ((Line (M1,i)),(Col (M2,j))))) by A9, MATRIX_3:6

.= 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 1;

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

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:13;
A26: len (Line (M1,i)) =
len M2
by A3, MATRIX_0:def 7

.= len (Col (M2,j)) by MATRIX_0:def 8 ;

A27: len (Line (M1,i)) = width M1 by MATRIX_0:def 7;

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:6

.= 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_0:def 8;

(Line (M1,i)) . k = M1 * (i,k) by A29, MATRIX_0:def 7;

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:60;

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:50;

((emb (m,L)) * (Line (M1,i))) . k = (emb (m,L)) * d by A23, A28, FVSUM_1:50;

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:50

.= (emb (m,L)) * (d * c) by GROUP_1:def 3

.= (emb (m,L)) * a by A23, A24, A28, FVSUM_1:60 ;

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:60; :: thesis: verum

end;.= len (Col (M2,j)) by MATRIX_0:def 8 ;

A27: len (Line (M1,i)) = width M1 by MATRIX_0:def 7;

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:6

.= 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_0:def 8;

(Line (M1,i)) . k = M1 * (i,k) by A29, MATRIX_0:def 7;

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:60;

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:50;

((emb (m,L)) * (Line (M1,i))) . k = (emb (m,L)) * d by A23, A28, FVSUM_1:50;

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:50

.= (emb (m,L)) * (d * c) by GROUP_1:def 3

.= (emb (m,L)) * a by A23, A24, A28, FVSUM_1:60 ;

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:60; :: thesis: verum

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 9 ;

hence (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) by A11, A32, FVSUM_1:73; :: thesis: verum

.= 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_0:21; :: thesis: verum