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

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