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