theorem :: MATRIX_5:1

1 = 1_ F_Complex by COMPLEX1:def 4, COMPLFLD:8;