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