let A be Matrix of REAL ; :: thesis: 1 * A = A
1 * A = MXF2MXR ((1_ F_Real ) * (MXR2MXF A)) by Def7;
hence 1 * A = A by MATRIX_5:10; :: thesis: verum