set e = 1_ F_Complex;
let M be Matrix of COMPLEX; :: thesis: 1 * M = M
1 * M = Field2COMPLEX ((1_ F_Complex) * (COMPLEX2Field M)) by Def7, COMPLEX1:def 4, COMPLFLD:8;
hence 1 * M = M by Th9; :: thesis: verum