A2: for b being set ex a being set st
( P₁[a] & P₂[b] ) by A1;
( ex a being set st P₁[a] & ( for b being set holds P₂[b] ) ) from SCHEMS_1:sch 10(A2);
hence ex a being set st
for b being set holds
( P₁[a] & P₂[b] ) ; :: thesis: verum