A2: ( F₂() is epsilon-transitive & F₂() is power-closed & F₂() is FamUnion-closed ) ;
deffunc H₁( set ) -> set = {F₃($1)};
consider s being Function such that
A3: ( dom s = F₁() & ( for X being set st X in F₁() holds
s . X = H₁(X) ) ) from FUNCT_1:sch 5();
rng s c= F₂()

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in F₂() )
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₃(x) in F₂() by A2, A1, A4, A3;
then A5: bool (bool F₃(x)) c= F₂() by A2;
H₁(x) c= bool F₃(x) by ZFMISC_1:68;
then H₁(x) in bool (bool F₃(x)) ;
then y in bool (bool F₃(x)) by A4, A3;
hence y in F₂() by A5; :: thesis: verum

end;

then A6: union (rng s) in F₂() by A3, A2, Def4;
set FX = { F₃(x) where x is Element of F₁() : x in F₁() } ;
A7: Union s c= { F₃(x) where x is Element of F₁() : x in F₁() }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union s or y in { F₃(x) where x is Element of F₁() : x in F₁() } )
assume y in Union s ; :: thesis: y in { F₃(x) where x is Element of F₁() : x 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₁(x) by A8, A3;
then y = F₃(x) by A8, TARSKI:def 1;
hence y in { F₃(x) where x is Element of F₁() : x in F₁() } by A8, A3; :: thesis: verum

end;

{ F₃(x) where x is Element of F₁() : x in F₁() } c= Union s

proof

let fx be object ; :: according to TARSKI:def 3 :: thesis: ( not fx in { F₃(x) where x is Element of F₁() : x in F₁() } or fx in Union s )
assume fx in { F₃(x) where x is Element of F₁() : x in F₁() } ; :: thesis: fx in Union s
then consider x being Element of F₁() such that
A9: ( fx = F₃(x) & x in F₁() ) ;
( fx in H₁(x) & H₁(x) = s . x ) by A9, A3, TARSKI:def 1;
hence fx in Union s by A9, A3, CARD_5:2; :: thesis: verum

end;

then { F₃(x) where x is Element of F₁() : x in F₁() } = Union s by A7;
hence { F₃(x) where x is Element of F₁() : x in F₁() } in F₂() by CARD_3:def 4, A6; :: thesis: verum