let NR, M be Matrix of 3,REAL; :: thesis: ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) is Matrix of 3,REAL

now :: thesis: ( (MXF2MXR ((MXR2MXF (NR @)) ~)) * M is Matrix of 3,REAL & MXF2MXR ((MXR2MXF NR) ~) is Matrix of 3,REAL )

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: MXF2MXR ((MXR2MXF NR) ~) is Matrix of 3,REAL
thus MXF2MXR ((MXR2MXF NR) ~) is Matrix of 3,REAL by MATRIXR1:def 2; :: thesis: verum

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: verum