assume not { F₂(a) where a is Element of F₁() : P₁[a] } = {} ; :: thesis: contradiction
then reconsider X = { F₂(a) where a is Element of F₁() : P₁[a] } as non empty set ;
consider x being Element of X;
x in X ;
then ex a being Element of F₁() st
( x = F₂(a) & P₁[a] ) ;
hence contradiction by A1; :: thesis: verum