let M be Matrix of COMPLEX ; :: thesis: (M + M) + M = 3 * M
reconsider e3 = ((1_ F_Complex ) + (1_ F_Complex )) + (1_ F_Complex ) as Element of F_Complex ;
A1: ( len M = len (COMPLEX2Field M) & width M = width (COMPLEX2Field M) ) ;
A2: (1_ F_Complex ) + (1_ F_Complex ) = the addF of F_Complex . (1_ F_Complex ),(1_ F_Complex ) by RLVECT_1:5
.= addcomplex . 1r ,1r by COMPLFLD:10, COMPLFLD:def 1
.= 1 + 1 by BINOP_2:def 3, COMPLEX1:def 7 ;
reconsider rr = 1 + 1 as Element of COMPLEX by XCMPLX_0:def 2;
((1_ F_Complex ) + (1_ F_Complex )) + (1_ F_Complex ) = the addF of F_Complex . ((1_ F_Complex ) + (1_ F_Complex )),(1_ F_Complex ) by RLVECT_1:5
.= addcomplex . (1 + 1),1 by A2, COMPLFLD:def 1
.= rr + 1 by BINOP_2:def 3, COMPLEX1:def 7
.= 3 ;
then 3 * M = Field2COMPLEX (e3 * (COMPLEX2Field M)) by Def7
.= Field2COMPLEX (((1_ F_Complex ) * (COMPLEX2Field M)) + (((1_ F_Complex ) + (1_ F_Complex )) * (COMPLEX2Field M))) by Th13
.= Field2COMPLEX ((COMPLEX2Field M) + (((1_ F_Complex ) + (1_ F_Complex )) * (COMPLEX2Field M))) by Th10
.= Field2COMPLEX ((COMPLEX2Field M) + (((1_ F_Complex ) * (COMPLEX2Field M)) + ((1_ F_Complex ) * (COMPLEX2Field M)))) by Th13
.= Field2COMPLEX ((COMPLEX2Field M) + ((COMPLEX2Field M) + ((1_ F_Complex ) * (COMPLEX2Field M)))) by Th10
.= Field2COMPLEX ((COMPLEX2Field M) + ((COMPLEX2Field M) + (COMPLEX2Field M))) by Th10
.= Field2COMPLEX (((COMPLEX2Field M) + (COMPLEX2Field M)) + (COMPLEX2Field M)) by A1, MATRIX_3:5 ;
hence (M + M) + M = 3 * M ; :: thesis: verum