assume
not { F_{2}(a) where a is Element of F_{1}() : P_{1}[a] } = {}
; :: thesis: contradiction

then reconsider X = { F_{2}(a) where a is Element of F_{1}() : P_{1}[a] } as non empty set ;

set x = the Element of X;

the Element of X in X ;

then ex a being Element of F_{1}() st

( the Element of X = F_{2}(a) & P_{1}[a] )
;

hence contradiction by A1; :: thesis: verum

then reconsider X = { F

set x = the Element of X;

the Element of X in X ;

then ex a being Element of F

( the Element of X = F

hence contradiction by A1; :: thesis: verum