let M be Matrix of COMPLEX ; :: thesis: M + M = 2 * M
reconsider e2 = (1_ F_Complex ) + (1_ F_Complex ) as Element of F_Complex ;
A1: (1_ F_Complex ) * (COMPLEX2Field M) = COMPLEX2Field M by Th10;
2 * M = Field2COMPLEX (e2 * (COMPLEX2Field M)) by Def7, COMPLEX1:def 7, COMPLFLD:10
.= Field2COMPLEX ((COMPLEX2Field M) + (COMPLEX2Field M)) by A1, Th13 ;
hence M + M = 2 * M ; :: thesis: verum