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