let f be Function; :: thesis: for x being object holds
( x in fixpoints f iff x is_a_fixpoint_of f )
let x be object ; :: thesis: ( x in fixpoints f iff x is_a_fixpoint_of f )
set FP = fixpoints f;
set D = dom f;
set I = id (dom f);
reconsider g = f /\ (id (dom f)) as Function ;
set y = g . x;
defpred S1[ object ] means $1 is_a_fixpoint_of f;
( (fixpoints f) \ (dom f) = {} & (fixpoints f) \ (dom (id (dom f))) = {} ) ;
then A1: ( fixpoints f c= dom f & fixpoints f c= dom (id (dom f)) ) by Th29;
thus ( x in fixpoints f implies S1[x] ) :: thesis: ( x is_a_fixpoint_of f implies x in fixpoints f )
proof
assume A2: x in fixpoints f ; :: thesis: S1[x]
[x,(g . x)] in g by A2, FUNCT_1:def 2;
then ( g . x = f . x & g . x = (id (dom f)) . x ) by FUNCT_1:def 2, A1, A2;
then f . x = x by FUNCT_1:17, A1, A2;
hence S1[x] by ABIAN:def 3, A1, A2; :: thesis: verum
end;
assume A3: S1[x] ; :: thesis: x in fixpoints f
then A4: ( x in dom f & x in dom (id (dom f)) & x = f . x ) by ABIAN:def 3;
( x = f . x & x = (id (dom f)) . x ) by A3, ABIAN:def 3, FUNCT_1:18;
then ( [x,x] in f & [x,x] in id (dom f) ) by A4, FUNCT_1:def 2;
then [x,x] in g by XBOOLE_0:def 4;
hence x in fixpoints f by XTUPLE_0:def 12; :: thesis: verum