ex y being Element of F₁() st
( F₂() = y & P₁[y] ) by A1;
hence P₁[F₂()] ; :: thesis: verum