set Y = { F2(z,F1()) where z is Element of F1() : P1[z,F1()] } ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in F1() or y in { F2(x,F1()) where x is Element of F1() : P1[x,F1()] } )
assume y in F1() ; :: thesis: y in { F2(x,F1()) where x is Element of F1() : P1[x,F1()] }
then consider x being set such that
A2: ( x in F1() & P1[x,F1()] & y = F2(x,F1()) ) by A1;
thus y in { F2(z,F1()) where z is Element of F1() : P1[z,F1()] } by A2; :: thesis: verum