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 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 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 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 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 Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2
thus for i being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 :: thesis: verum

proof

let i be 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_0:def 7;
then A6: len ((Line (M1,i)) * M2) = width M2 by MATRIXR1:62;
len (Line (M,i)) = width M by MATRIX_0: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_0:def 7;
then A11: [i,j] in Indices M by A4, Th12;
A12: (M . i) . j in REAL by XREAL_0:def 1;
thus (Line (M,i)) . j = (M . i) . j by A8, MATRIX_0:60
.= M * (i,j) by A11, MATRIX_0:def 5, A12
.= (Line (M1,i)) "*" (Col (M2,j)) by A1, A2, 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
A13: len M = len M1 and
A14: width M = width M2 and
A15: for i being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ; :: thesis: M = M1 * M2
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) )
assume A16: [i,j] in Indices M ; :: thesis: M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
A17: i in Seg (len M) by A16, Th12;
then A18: i in dom M by FINSEQ_1:def 3;
A19: len (Line (M1,i)) = len M2 by A1, MATRIX_0:def 7;
j in Seg (width M) by A16, Th12;
then A20: j in Seg (len ((Line (M1,i)) * M2)) by A14, A19, MATRIXR1:62;
(M . i) . j in REAL by XREAL_0:def 1;
hence M * (i,j) = (M . i) . j by A16, MATRIX_0:def 5
.= (Line (M,i)) . j by A18, MATRIX_0:60
.= ((Line (M1,i)) * M2) . j by A15, A17
.= (Line (M1,i)) "*" (Col (M2,j)) by A19, A20, Th40 ;
:: thesis: verum

end;

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