defpred S₁[ set , set ] means ( ( P₁[$1] implies $2 = F₂($1) ) & ( P₁[$1] implies $2 = F₃($1) ) );

A1: now

let i be set ; :: thesis: ( i in F₁() implies ex j being set st S₁[i,j] )
assume i in F₁() ; :: thesis: ex j being set st S₁[i,j]
thus ex j being set st S₁[i,j] :: thesis: verum

proof

per cases ( P₁[i] or not P₁[i] ) ;

suppose A2: P₁[i] ; :: thesis: ex j being set st S₁[i,j]

take F₂(i) ; :: thesis: S₁[i,F₂(i)]
thus S₁[i,F₂(i)] by A2; :: thesis: verum

end;

suppose A3: P₁[i] ; :: thesis: ex j being set st S₁[i,j]

take F₃(i) ; :: thesis: S₁[i,F₃(i)]
thus S₁[i,F₃(i)] by A3; :: thesis: verum

end;

end;

end;

end;

consider f being ManySortedSet of such that
A4: for i being set st i in F₁() holds
S₁[i,f . i] from PBOOLE:sch 3(A1);
take f ; :: thesis: for i being Element of F₁() st i in F₁() holds
( ( P₁[i] implies f . i = F₂(i) ) & ( P₁[i] implies f . i = F₃(i) ) )
thus for i being Element of F₁() st i in F₁() holds
( ( P₁[i] implies f . i = F₂(i) ) & ( P₁[i] implies f . i = F₃(i) ) ) by A4; :: thesis: verum