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 Element of 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 Element of NAT st [i,j] in Indices M holds
M * i,j = (Line M1,i) "*" (Col M2,j) ) ) )
set M3 = MXR2MXF M1;
set M4 = MXR2MXF M2;
A2: ( MXR2MXF M1 = M1 & MXR2MXF M2 = M2 ) by MATRIXR1:def 1;
MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) = M1 * M2 by MATRIXR1:def 6;
then A3: (MXR2MXF M1) * (MXR2MXF M2) = M1 * M2 by MATRIXR1:def 2;

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

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

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 A7: [i,j] in Indices M ; :: thesis: M * i,j = (Line M1,i) "*" (Col M2,j)
A8: ( i in Seg (len M1) & j in Seg (width M2) ) by A5, A6, A7, Th12;
then i in dom M1 by FINSEQ_1:def 3;
then A9: Line (MXR2MXF M1),i = Line M1,i by A2, Th16;
A10: Col (MXR2MXF M2),j = Col M2,j by A2, A8, Th17;
A11: len (Line M1,i) = width M1 by MATRIX_1:def 8
.= len (Col M2,j) by A1, MATRIX_1:def 9 ;
M = MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) by A4, MATRIXR1:def 6;
then ( [i,j] in Indices ((MXR2MXF M1) * (MXR2MXF M2)) & M * i,j = ((MXR2MXF M1) * (MXR2MXF M2)) * i,j ) by A7, MATRIXR1:23, MATRIXR1:def 2;
hence M * i,j = (Line (MXR2MXF M1),i) "*" (Col (MXR2MXF M2),j) by A1, A2, MATRIX_3:def 4
.= (Line M1,i) "*" (Col M2,j) by A9, A10, A11, Th38 ;
:: thesis: verum

end;

end;

assume A12: ( len M = len M1 & width M = width M2 & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (Line M1,i) "*" (Col M2,j) ) ) ; :: thesis: M = M1 * M2
set MM = MXR2MXF M;
A13: MXR2MXF M = M by MATRIXR1:def 1;
MXR2MXF M = (MXR2MXF M1) * (MXR2MXF M2)

proof

A14: len (MXR2MXF M) = len M by MATRIXR1:def 1
.= len (MXR2MXF M1) by A12, MATRIXR1:def 1 ;
A15: width (MXR2MXF M) = width M by MATRIXR1:def 1
.= width (MXR2MXF M2) 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 A16: [i,j] in Indices (MXR2MXF M) ; :: thesis: (MXR2MXF M) * i,j = (Line (MXR2MXF M1),i) "*" (Col (MXR2MXF M2),j)
A17: ( i in NAT & j in NAT ) by ORDINAL1:def 13;
then A18: ( i in Seg (len (MXR2MXF M1)) & j in Seg (width (MXR2MXF M2)) ) by A14, A15, A16, 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: Col (MXR2MXF M2),j = Col M2,j by A18, Th17, MATRIXR1:def 1;
A21: len (Line M1,i) = width M1 by MATRIX_1:def 8
.= len (Col M2,j) by A1, MATRIX_1:def 9 ;
( [i,j] in Indices M & (MXR2MXF M) * i,j = M * i,j ) by A16, MATRIXR1:23, MATRIXR1:def 1;
hence (MXR2MXF M) * i,j = (Line M1,i) "*" (Col M2,j) by A12, A17
.= (Line (MXR2MXF M1),i) "*" (Col (MXR2MXF M2),j) by A19, A20, A21, Th38 ;
:: thesis: verum

end;

hence MXR2MXF M = (MXR2MXF M1) * (MXR2MXF M2) by A1, A2, A14, A15, MATRIX_3:def 4; :: thesis: verum

end;

then M = MXF2MXR ((MXR2MXF M1) * (MXR2MXF M2)) by A13, MATRIXR1:def 2;
hence M = M1 * M2 by MATRIXR1:def 6; :: thesis: verum