A1: rng (1_. F_Complex) c= (rng (0_. F_Complex)) \/ {(1. F_Complex)} by FUNCT_7:100;
1. F_Complex = 1 by COMPLFLD:def 1;
hence rng (1_. F_Complex) c= INT by A1, INT_1:def 2; :: according to RELAT_1:def 19 :: thesis: verum