defpred S₁[ set , set ] means P₁[$1,$2];
A2: for i being set st i in F₁() holds
ex j being set st S₁[i,j] by A1;
consider f being ManySortedSet of F₁() such that
A3: for i being set st i in F₁() holds
S₁[i,f . i] from PBOOLE:sch 3(A2);
take f ; :: thesis: for i being Element of F₁() holds P₁[i,f . i]
let i be Element of F₁(); :: thesis: P₁[i,f . i]
thus P₁[i,f . i] by A3; :: thesis: verum