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 Th8
.= z ;
:: thesis: verum