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:9; :: thesis: verum