A2:
( F_{2}() is epsilon-transitive & F_{2}() is power-closed & F_{2}() is FamUnion-closed )
;

deffunc H_{1}( set ) -> set = {F_{3}($1)};

consider s being Function such that

A3: ( dom s = F_{1}() & ( for X being set st X in F_{1}() holds

s . X = H_{1}(X) ) )
from FUNCT_1:sch 5();

rng s c= F_{2}()
_{2}()
by A3, A2, Def4;

set FX = { F_{3}(x) where x is Element of F_{1}() : x in F_{1}() } ;

A7: Union s c= { F_{3}(x) where x is Element of F_{1}() : x in F_{1}() }
_{3}(x) where x is Element of F_{1}() : x in F_{1}() } c= Union s
_{3}(x) where x is Element of F_{1}() : x in F_{1}() } = Union s
by A7;

hence { F_{3}(x) where x is Element of F_{1}() : x in F_{1}() } in F_{2}()
by CARD_3:def 4, A6; :: thesis: verum

deffunc H

consider s being Function such that

A3: ( dom s = F

s . X = H

rng s c= F

proof

then A6:
union (rng s) in F
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in F_{2}() )

assume y in rng s ; :: thesis: y in F_{2}()

then consider x being object such that

A4: ( x in dom s & s . x = y ) by FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

bool F_{3}(x) in F_{2}()
by A2, A1, A4, A3;

then A5: bool (bool F_{3}(x)) c= F_{2}()
by A2;

H_{1}(x) c= bool F_{3}(x)
by ZFMISC_1:68;

then H_{1}(x) in bool (bool F_{3}(x))
;

then y in bool (bool F_{3}(x))
by A4, A3;

hence y in F_{2}()
by A5; :: thesis: verum

end;assume y in rng s ; :: thesis: y in F

then consider x being object such that

A4: ( x in dom s & s . x = y ) by FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

bool F

then A5: bool (bool F

H

then H

then y in bool (bool F

hence y in F

set FX = { F

A7: Union s c= { F

proof

{ F
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union s or y in { F_{3}(x) where x is Element of F_{1}() : x in F_{1}() } )

assume y in Union s ; :: thesis: y in { F_{3}(x) where x is Element of F_{1}() : x in F_{1}() }

then consider x being object such that

A8: ( x in dom s & y in s . x ) by CARD_5:2;

reconsider x = x as set by TARSKI:1;

s . x = H_{1}(x)
by A8, A3;

then y = F_{3}(x)
by A8, TARSKI:def 1;

hence y in { F_{3}(x) where x is Element of F_{1}() : x in F_{1}() }
by A8, A3; :: thesis: verum

end;assume y in Union s ; :: thesis: y in { F

then consider x being object such that

A8: ( x in dom s & y in s . x ) by CARD_5:2;

reconsider x = x as set by TARSKI:1;

s . x = H

then y = F

hence y in { F

proof

then
{ F
let fx be object ; :: according to TARSKI:def 3 :: thesis: ( not fx in { F_{3}(x) where x is Element of F_{1}() : x in F_{1}() } or fx in Union s )

assume fx in { F_{3}(x) where x is Element of F_{1}() : x in F_{1}() }
; :: thesis: fx in Union s

then consider x being Element of F_{1}() such that

A9: ( fx = F_{3}(x) & x in F_{1}() )
;

( fx in H_{1}(x) & H_{1}(x) = s . x )
by A9, A3, TARSKI:def 1;

hence fx in Union s by A9, A3, CARD_5:2; :: thesis: verum

end;assume fx in { F

then consider x being Element of F

A9: ( fx = F

( fx in H

hence fx in Union s by A9, A3, CARD_5:2; :: thesis: verum

hence { F