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