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, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) ) )
assume A1: width M1 = len M2 ; :: thesis: ( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) )
set MM = MXR2MXF M;
set M4 = MXR2MXF M2;
set M3 = MXR2MXF M1;
A2: MXR2MXF M1 = M1 by MATRIXR1:def 1;
A3: MXR2MXF M2 = M2 by MATRIXR1:def 1;
MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) = M1 * M2 by MATRIXR1:def 6;
then A4: (MXR2MXF M1) * (MXR2MXF M2) = M1 * M2 by MATRIXR1:def 2;

hereby :: thesis: ( len M = len M1 & width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) implies M = M1 * M2 )

assume A5: M = M1 * M2 ; :: thesis: ( len M = len M1 & width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) )
hence A6: len M = len M1 by A1, A2, A3, A4, MATRIX_3:def 4; :: thesis: ( width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) )
thus A7: width M = width M2 by A1, A2, A3, A4, A5, MATRIX_3:def 4; :: thesis: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
thus for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) :: thesis: verum

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) )
assume A8: [i,j] in Indices M ; :: thesis: M * (i,j) = (Line (M1,i)) "*" (Col (M2,j))
j in Seg (width M2) by A7, A8, Th12;
then A9: Col ((MXR2MXF M2),j) = Col (M2,j) by A3, Th17;
i in Seg (len M1) by A6, A8, Th12;
then i in dom M1 by FINSEQ_1:def 3;
then A10: Line ((MXR2MXF M1),i) = Line (M1,i) by A2, Th16;
A11: len (Line (M1,i)) = width M1 by MATRIX_0:def 7
.= len (Col (M2,j)) by A1, MATRIX_0:def 8 ;
M = MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) by A5, MATRIXR1:def 6;
then ( [i,j] in Indices ((MXR2MXF M1) * (MXR2MXF M2)) & M * (i,j) = ((MXR2MXF M1) * (MXR2MXF M2)) * (i,j) ) by A8, MATRIXR1:23, MATRIXR1:def 2;
hence M * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j)) by A1, A2, A3, MATRIX_3:def 4
.= (Line (M1,i)) "*" (Col (M2,j)) by A10, A9, A11, Th38 ;
:: thesis: verum

end;

end;

assume that
A12: len M = len M1 and
A13: width M = width M2 and
A14: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ; :: thesis: M = M1 * M2
A15: width (MXR2MXF M) = width M by MATRIXR1:def 1
.= width (MXR2MXF M2) by A13, MATRIXR1:def 1 ;
A16: len (MXR2MXF M) = len M by MATRIXR1:def 1
.= len (MXR2MXF M1) by A12, MATRIXR1:def 1 ;
for i, j being Nat st [i,j] in Indices (MXR2MXF M) holds
(MXR2MXF M) * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (MXR2MXF M) implies (MXR2MXF M) * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j)) )
assume A17: [i,j] in Indices (MXR2MXF M) ; :: thesis: (MXR2MXF M) * (i,j) = (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j))
j in Seg (width (MXR2MXF M2)) by A15, A17, Th12;
then A18: Col ((MXR2MXF M2),j) = Col (M2,j) by Th17, MATRIXR1:def 1;
i in Seg (len (MXR2MXF M1)) by A16, A17, Th12;
then i in dom (MXR2MXF M1) by FINSEQ_1:def 3;
then A19: Line ((MXR2MXF M1),i) = Line (M1,i) by Th16, MATRIXR1:def 1;
A20: len (Line (M1,i)) = width M1 by MATRIX_0:def 7
.= len (Col (M2,j)) by A1, MATRIX_0:def 8 ;
( [i,j] in Indices M & (MXR2MXF M) * (i,j) = M * (i,j) ) by A17, MATRIXR1:23, MATRIXR1:def 1;
hence (MXR2MXF M) * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) by A14
.= (Line ((MXR2MXF M1),i)) "*" (Col ((MXR2MXF M2),j)) by A19, A18, A20, Th38 ;
:: thesis: verum

end;

then ( MXR2MXF M = M & MXR2MXF M = (MXR2MXF M1) * (MXR2MXF M2) ) by A1, A2, A3, A16, A15, MATRIXR1:def 1, MATRIX_3:def 4;
then M = MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) by MATRIXR1:def 2;
hence M = M1 * M2 by MATRIXR1:def 6; :: thesis: verum