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 7;
then A6: len ((Line (M1,i)) * M2) = width M2 by MATRIXR1:62;
len (Line (M,i)) = width M by MATRIX_1:def 7;
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 7;
then A11: [i,j] in Indices M by A4, Th12;
thus (Line (M,i)) . j = (M . i) . j by A8, MATRIX_2:16
.= M * (i,j) by A11, MATRIX_1:def 5
.= (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:13; :: 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 7;
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 5
.= (Line (M,i)) . j by A17, MATRIX_2:16
.= ((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