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

proof

let x be object ; :: thesis: ( x in F₄(F₂()) \/ F₄(F₃()) iff ex Y being set st
( x in Y & Y in { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} } ) )
thus ( x in F₄(F₂()) \/ F₄(F₃()) implies ex Y being set st
( x in Y & Y in { F₄(j) where j is Element of F₁() : j 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₂(),F₃()} } ) implies x in F₄(F₂()) \/ F₄(F₃()) )

proof

assume x in F₄(F₂()) \/ F₄(F₃()) ; :: thesis: ex Y being set st
( x in Y & Y in { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} } )

per cases then ( x in F₄(F₂()) or x in F₄(F₃()) ) by XBOOLE_0:def 3;

suppose 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₂(),F₃()} } )

take F₄(F₂()) ; :: thesis: ( x in F₄(F₂()) & F₄(F₂()) in { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} } )
thus x in F₄(F₂()) by A1; :: thesis: F₄(F₂()) in { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} }
F₂() in {F₂(),F₃()} by TARSKI:def 2;
hence F₄(F₂()) in { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} } ; :: thesis: verum

end;

suppose A2: 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₂(),F₃()} } )

take F₄(F₃()) ; :: thesis: ( x in F₄(F₃()) & F₄(F₃()) in { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} } )
thus x in F₄(F₃()) by A2; :: thesis: F₄(F₃()) in { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} }
F₃() in {F₂(),F₃()} by TARSKI:def 2;
hence F₄(F₃()) in { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} } ; :: thesis: verum

end;

end;

end;

given Y being set such that A3: x in Y and
A4: Y in { F₄(j) where j is Element of F₁() : j in {F₂(),F₃()} } ; :: thesis: x in F₄(F₂()) \/ F₄(F₃())
consider j being Element of F₁() such that
A5: Y = F₄(j) and
A6: j in {F₂(),F₃()} by A4;

now :: thesis: ( ( j = F₂() & x in F₄(F₂()) ) or ( j = F₃() & x in F₄(F₃()) ) )

per cases ( j = F₂() or j = F₃() ) by A6, TARSKI:def 2;

case j = F₂() ; :: thesis: x in F₄(F₂())

hence x in F₄(F₂()) by A3, A5; :: thesis: verum

end;

case j = F₃() ; :: thesis: x in F₄(F₃())

hence x in F₄(F₃()) by A3, A5; :: thesis: verum

end;

end;

end;

hence x in F₄(F₂()) \/ F₄(F₃()) by XBOOLE_0:def 3; :: thesis: verum

end;

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