consider f being Function such that
A3: ( dom f = bool F1() & ( for x being object st x in bool F1() holds
f . x = F2(x) ) ) from FUNCT_1:sch 3();
 rng f c= bool F1()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in bool F1() )
assume x in rng f ; :: thesis: x in bool F1()
then consider y being object such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def 3;
F2(y) c= F2(F1()) by A1, A3, A4;
then F2(y) c= F1() by A2;
then f . y c= F1() by A3, A4;
hence x in bool F1() by A5; :: thesis: verum
end;
then reconsider f = f as Function of (bool F1()),(bool F1()) by A3, FUNCT_2:def 1, RELSET_1:4;
now :: thesis: for a, b being set st a in dom f & b in dom f & a c= b holds
f . a c= f . b
let a, b be set ; :: thesis: ( a in dom f & b in dom f & a c= b implies f . a c= f . b )
assume that
A6: ( a in dom f & b in dom f ) and
A7: a c= b ; :: thesis: f . a c= f . b
( f . a = F2(a) & f . b = F2(b) ) by A3, A6;
hence f . a c= f . b by A1, A7; :: thesis: verum
end;
then reconsider f = f as V224() Function of (bool F1()),(bool F1()) by COHSP_1:def 11;
take d = lfp (F1(),f); :: thesis: ( F2(d) = d & d c= F1() )
d is_a_fixpoint_of f by Th4;
then d = f . d ;
hence F2(d) = d by A3; :: thesis: d c= F1()
thus d c= F1() ; :: thesis: verum