let z be Element of F_Complex; :: thesis: z / (1. F_Complex) = z
reconsider z1 = z as Element of COMPLEX by Def1;
1. F_Complex = 1r by Def1;
hence z / (1. F_Complex) = z1 / 1r by Th6
.= z ;
:: thesis: verum