defpred S₁[ set , Element of Fin F₁()] means for a being Element of F₁() holds
( a in $2 iff ( a in F₂() & P₁[a,$1] ) );

A1: now :: thesis: for x being Element of F₁() ex y9 being Element of Fin F₁() st S₁[x,y9]

reconsider B = F₂() as Subset of F₁() by FINSUB_1:def 5;
let x be Element of F₁(); :: thesis: ex y9 being Element of Fin F₁() st S₁[x,y9]
defpred S₂[ set ] means ( $1 in F₂() & P₁[$1,x] );
consider y being Subset of F₁() such that
A2: for a being Element of F₁() holds
( a in y iff S₂[a] ) from SUBSET_1:sch 3();
for x being Element of F₁() st x in y holds
x in B by A2;
then y c= F₂() ;
then reconsider y = y as Element of Fin F₁() by FINSUB_1:def 5;
take y9 = y; :: thesis: S₁[x,y9]
thus S₁[x,y9] by A2; :: thesis: verum

end;

thus ex f being Function of F₁(),(Fin F₁()) st
for x being Element of F₁() holds S₁[x,f . x] from FUNCT_2:sch 3(A1); :: thesis: verum