0. F_Complex = 0c by Def1;
hence (0. F_Complex) *' = 0. F_Complex by COMPLEX1:28; :: thesis: verum