let NR, M be Matrix of 3,REAL; :: thesis:

now :: thesis:

reconsider M6 = MXF2MXR ((MXR2MXF (NR @)) ~) as Matrix of 3,REAL by MATRIXR1:def 2;
M6 * M is Matrix of 3,REAL ;
hence (MXF2MXR ((MXR2MXF (NR @)) ~)) * M is Matrix of 3,REAL ; :: thesis:
thus MXF2MXR ((MXR2MXF NR) ~) is Matrix of 3,REAL by MATRIXR1:def 2; :: thesis:

end;

then reconsider M3 = (MXF2MXR ((MXR2MXF (NR @)) ~)) * M, M4 = MXF2MXR ((MXR2MXF NR) ~) as Matrix of 3,REAL ;
M3 * M4 is Matrix of 3,REAL ;
hence ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) is Matrix of 3,REAL ; :: thesis: