set e2 = (1_ F_Real) + (1_ F_Real);
let A be Matrix of REAL; :: thesis: A + A = 2 * A
A1: (1_ F_Real) * (MXR2MXF A) = MXR2MXF A by MATRIX_5:9;
2 * A = MXF2MXR (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A)) by Def7
.= MXF2MXR ((MXR2MXF A) + (MXR2MXF A)) by A1, MATRIX_5:12 ;
hence A + A = 2 * A ; :: thesis: verum