let M, M1, M2 be Matrix of REAL ; :: thesis: ( width M1 = len M2 implies ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 ) ) ) )
assume A1: width M1 = len M2 ; :: thesis: ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 ) ) )

hereby :: thesis: ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 ) implies M = M1 * M2 )

assume A2: M = M1 * M2 ; :: thesis: ( len M = len M1 & width M = width M2 & ( for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 ) )
hence A3: ( len M = len M1 & width M = width M2 ) by A1, Th39; :: thesis: for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2
thus for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( i in Seg (len M) implies Line M,i = (Line M1,i) * M2 )
assume A4: i in Seg (len M) ; :: thesis: Line M,i = (Line M1,i) * M2
A5: len (Line M1,i) = len M2 by A1, MATRIX_1:def 8;
then A6: len ((Line M1,i) * M2) = width M2 by MATRIXR1:62;
len (Line M,i) = width M by MATRIX_1:def 8;
then A7: dom (Line M,i) = Seg (width M2) by A3, FINSEQ_1:def 3
.= dom ((Line M1,i) * M2) by A6, FINSEQ_1:def 3 ;
A8: i in dom M by A4, FINSEQ_1:def 3;
for j being Nat st j in dom (Line M,i) holds
(Line M,i) . j = ((Line M1,i) * M2) . j

proof

let j be Nat; :: thesis: ( j in dom (Line M,i) implies (Line M,i) . j = ((Line M1,i) * M2) . j )
assume A9: j in dom (Line M,i) ; :: thesis: (Line M,i) . j = ((Line M1,i) * M2) . j
A10: j in Seg (len ((Line M1,i) * M2)) by A7, A9, FINSEQ_1:def 3;
j in Seg (len (Line M,i)) by A9, FINSEQ_1:def 3;
then j in Seg (width M) by MATRIX_1:def 8;
then A11: [i,j] in Indices M by A4, Th12;
thus (Line M,i) . j = (M . i) . j by A8, MATRIX_2:18
.= M * i,j by A11, MATRIX_1:def 6
.= (Line M1,i) "*" (Col M2,j) by A1, A2, A9, A11, Th39
.= ((Line M1,i) * M2) . j by A5, A10, Th40 ; :: thesis: verum

end;

hence Line M,i = (Line M1,i) * M2 by A7, FINSEQ_1:17; :: thesis: verum

end;

end;

assume that
A12: len M = len M1 and
A13: width M = width M2 and
A14: for i being Element of NAT st i in Seg (len M) holds
Line M,i = (Line M1,i) * M2 ; :: thesis: M = M1 * M2
for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (Line M1,i) "*" (Col M2,j)

proof

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices M implies M * i,j = (Line M1,i) "*" (Col M2,j) )
assume A15: [i,j] in Indices M ; :: thesis: M * i,j = (Line M1,i) "*" (Col M2,j)
A16: i in Seg (len M) by A15, Th12;
then A17: i in dom M by FINSEQ_1:def 3;
A18: len (Line M1,i) = len M2 by A1, MATRIX_1:def 8;
j in Seg (width M) by A15, Th12;
then A19: j in Seg (len ((Line M1,i) * M2)) by A13, A18, MATRIXR1:62;
thus M * i,j = (M . i) . j by A15, MATRIX_1:def 6
.= (Line M,i) . j by A17, MATRIX_2:18
.= ((Line M1,i) * M2) . j by A14, A16
.= (Line M1,i) "*" (Col M2,j) by A18, A19, Th40 ; :: thesis: verum

end;

hence M = M1 * M2 by A1, A12, A13, Th39; :: thesis: verum