set X = { F3(j) where j is Element of F1() : j in {F2()} } ;
for x being object holds
( x in F3(F2()) iff ex Y being set st
( x in Y & Y in { F3(j) where j is Element of F1() : j in {F2()} } ) )
proof
let x be object ; :: thesis: ( x in F3(F2()) iff ex Y being set st
( x in Y & Y in { F3(j) where j is Element of F1() : j in {F2()} } ) )
thus ( x in F3(F2()) implies ex Y being set st
( x in Y & Y in { F3(j) where j is Element of F1() : j in {F2()} } ) ) :: thesis: ( ex Y being set st
( x in Y & Y in { F3(j) where j is Element of F1() : j in {F2()} } ) implies x in F3(F2()) )
proof
assume A1: x in F3(F2()) ; :: thesis: ex Y being set st
( x in Y & Y in { F3(j) where j is Element of F1() : j in {F2()} } )
take F3(F2()) ; :: thesis: ( x in F3(F2()) & F3(F2()) in { F3(j) where j is Element of F1() : j in {F2()} } )
thus x in F3(F2()) by A1; :: thesis: F3(F2()) in { F3(j) where j is Element of F1() : j in {F2()} }
F2() in {F2()} by TARSKI:def 1;
hence F3(F2()) in { F3(j) where j is Element of F1() : j in {F2()} } ; :: thesis: verum
end;
given Y being set such that A2: x in Y and
A3: Y in { F3(j) where j is Element of F1() : j in {F2()} } ; :: thesis: x in F3(F2())
ex j being Element of F1() st
( Y = F3(j) & j in {F2()} ) by A3;
hence x in F3(F2()) by A2, TARSKI:def 1; :: thesis: verum
end;
hence union { F3(j) where j is Element of F1() : j in {F2()} } = F3(F2()) by TARSKI:def 4; :: thesis: verum