f " = f ~ by FUNCT_1:def 5;
hence (fixpoints1 (f ")) \+\ (fixpoints1 f) is empty ; :: thesis: verum