1. F_Complex = 1r " by Def1;
hence (1. F_Complex) " = 1. F_Complex by Th5; :: thesis: verum