A2: for i being object st i in F₁() holds
ex j being object st P₁[i,j] by A1;
consider f being ManySortedSet of F₁() such that
A3: for i being object st i in F₁() holds
P₁[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