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