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