consider f being Function such that
A3: ( dom f = bool F₁() & ( for x being set st x in bool F₁() holds
f . x = F₂(x) ) ) from FUNCT_1:sch 3();
rng f c= bool F₁()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in bool F₁() )
assume x in rng f ; :: thesis: x in bool F₁()
then consider y being set such that
A4: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
F₂(y) c= F₂(F₁()) by A1, A3, A4;
then F₂(y) c= F₁() by A2, XBOOLE_1:1;
then f . y c= F₁() by A3, A4;
hence x in bool F₁() by A4; :: thesis: verum

end;

then reconsider f = f as Function of (bool F₁()),(bool F₁()) by A3, FUNCT_2:def 1, RELSET_1:11;

now

let a, b be set ; :: thesis: ( a in dom f & b in dom f & a c= b implies f . a c= f . b )
assume A5: ( a in dom f & b in dom f & a c= b ) ; :: thesis: f . a c= f . b
then ( f . a = F₂(a) & f . b = F₂(b) ) by A3;
hence f . a c= f . b by A1, A5; :: thesis: verum

end;

then reconsider f = f as V202() Function of (bool F₁()),(bool F₁()) by COHSP_1:def 12;
take d = lfp F₁(),f; :: thesis: ( F₂(d) = d & d c= F₁() )
d is_a_fixpoint_of f by Th6;
then d = f . d by ABIAN:def 3;
hence F₂(d) = d by A3; :: thesis: d c= F₁()
thus d c= F₁() ; :: thesis: verum