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