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