reconsider e3 = ((1_ F_Real) + (1_ F_Real)) + (1_ F_Real) as Element of F_Real ;
let A be Matrix of REAL; :: thesis: (A + A) + A = 3 * A
A1: ( len A = len (MXR2MXF A) & width A = width (MXR2MXF A) ) ;
3 * A = MXF2MXR (e3 * (MXR2MXF A)) by Def7
.= MXF2MXR (((1_ F_Real) * (MXR2MXF A)) + (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A))) by MATRIX_5:12
.= MXF2MXR ((MXR2MXF A) + (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A))) by MATRIX_5:9
.= MXF2MXR ((MXR2MXF A) + (((1_ F_Real) * (MXR2MXF A)) + ((1_ F_Real) * (MXR2MXF A)))) by MATRIX_5:12
.= MXF2MXR ((MXR2MXF A) + ((MXR2MXF A) + ((1_ F_Real) * (MXR2MXF A)))) by MATRIX_5:9
.= MXF2MXR ((MXR2MXF A) + ((MXR2MXF A) + (MXR2MXF A))) by MATRIX_5:9
.= MXF2MXR (((MXR2MXF A) + (MXR2MXF A)) + (MXR2MXF A)) by A1, MATRIX_3:3 ;
hence (A + A) + A = 3 * A ; :: thesis: verum