consider f being Function such that

A3: ( dom f = bool F_{1}() & ( for x being object st x in bool F_{1}() holds

f . x = F_{2}(x) ) )
from FUNCT_1:sch 3();

rng f c= bool F_{1}()
_{1}()),(bool F_{1}()) by A3, FUNCT_2:def 1, RELSET_1:4;

_{1}()),(bool F_{1}()) by COHSP_1:def 11;

take d = lfp (F_{1}(),f); :: thesis: ( F_{2}(d) = d & d c= F_{1}() )

d is_a_fixpoint_of f by Th4;

then d = f . d ;

hence F_{2}(d) = d
by A3; :: thesis: d c= F_{1}()

thus d c= F_{1}()
; :: thesis: verum

A3: ( dom f = bool F

f . x = F

rng f c= bool F

proof

then reconsider f = f as Function of (bool F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in bool F_{1}() )

assume x in rng f ; :: thesis: x in bool F_{1}()

then consider y being object such that

A4: y in dom f and

A5: x = f . y by FUNCT_1:def 3;

F_{2}(y) c= F_{2}(F_{1}())
by A1, A3, A4;

then F_{2}(y) c= F_{1}()
by A2;

then f . y c= F_{1}()
by A3, A4;

hence x in bool F_{1}()
by A5; :: thesis: verum

end;assume x in rng f ; :: thesis: x in bool F

then consider y being object such that

A4: y in dom f and

A5: x = f . y by FUNCT_1:def 3;

F

then F

then f . y c= F

hence x in bool F

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

then reconsider f = f as V224() Function of (bool Ff . 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 = F_{2}(a) & f . b = F_{2}(b) )
by A3, A6;

hence f . a c= f . b by A1, A7; :: thesis: verum

end;assume that

A6: ( a in dom f & b in dom f ) and

A7: a c= b ; :: thesis: f . a c= f . b

( f . a = F

hence f . a c= f . b by A1, A7; :: thesis: verum

take d = lfp (F

d is_a_fixpoint_of f by Th4;

then d = f . d ;

hence F

thus d c= F