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