set X = { F₃(j) where j is Element of F₁() : j in {F₂()} } ;
for x being object holds
( x in F₃(F₂()) iff ex Y being set st
( x in Y & Y in { F₃(j) where j is Element of F₁() : j in {F₂()} } ) )

proof

let x be object ; :: thesis: ( x in F₃(F₂()) iff ex Y being set st
( x in Y & Y in { F₃(j) where j is Element of F₁() : j in {F₂()} } ) )
thus ( x in F₃(F₂()) implies ex Y being set st
( x in Y & Y in { F₃(j) where j is Element of F₁() : j in {F₂()} } ) ) :: thesis: ( ex Y being set st
( x in Y & Y in { F₃(j) where j is Element of F₁() : j in {F₂()} } ) implies x in F₃(F₂()) )

proof

assume A1: x in F₃(F₂()) ; :: thesis: ex Y being set st
( x in Y & Y in { F₃(j) where j is Element of F₁() : j in {F₂()} } )
take F₃(F₂()) ; :: thesis: ( x in F₃(F₂()) & F₃(F₂()) in { F₃(j) where j is Element of F₁() : j in {F₂()} } )
thus x in F₃(F₂()) by A1; :: thesis: F₃(F₂()) in { F₃(j) where j is Element of F₁() : j in {F₂()} }
F₂() in {F₂()} by TARSKI:def 1;
hence F₃(F₂()) in { F₃(j) where j is Element of F₁() : j in {F₂()} } ; :: thesis: verum

end;

given Y being set such that A2: x in Y and
A3: Y in { F₃(j) where j is Element of F₁() : j in {F₂()} } ; :: thesis: x in F₃(F₂())
ex j being Element of F₁() st
( Y = F₃(j) & j in {F₂()} ) by A3;
hence x in F₃(F₂()) by A2, TARSKI:def 1; :: thesis: verum

end;

hence union { F₃(j) where j is Element of F₁() : j in {F₂()} } = F₃(F₂()) by TARSKI:def 4; :: thesis: verum