1. F_Complex = 1r by Def1;
hence (1. F_Complex ) *' = 1. F_Complex by COMPLEX1:115; :: thesis: verum