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 7, COMPLFLD:10;
hence 1 * M = M by Th10; :: thesis: verum