defpred S₁[ set , set ] means ( P₁[$2,$1] & ( for i' being Element of F₁() st $1 = i' holds
$2 in the carrier of (F₂() . i') ) );
A2: for i being set st i in F₁() holds
ex x being set st S₁[i,x]

proof

let i be set ; :: thesis: ( i in F₁() implies ex x being set st S₁[i,x] )
assume i in F₁() ; :: thesis: ex x being set st S₁[i,x]
then reconsider i1 = i as Element of F₁() ;
consider x being Element of such that
A3: P₁[x,i1] by A1;
take x ; :: thesis: S₁[i,x]
thus P₁[x,i] by A3; :: thesis: for i' being Element of F₁() st i = i' holds
x in the carrier of (F₂() . i')
let i' be Element of F₁(); :: thesis: ( i = i' implies x in the carrier of (F₂() . i') )
assume i = i' ; :: thesis: x in the carrier of (F₂() . i')
hence x in the carrier of (F₂() . i') ; :: thesis: verum

end;

consider f being Function such that
A4: dom f = F₁() and
A5: for i being set st i in F₁() holds
S₁[i,f . i] from CLASSES1:sch 1(A2);
A6: for x being set st x in dom (Carrier F₂()) holds
f . x in (Carrier F₂()) . x

proof

let x be set ; :: thesis: ( x in dom (Carrier F₂()) implies f . x in (Carrier F₂()) . x )
assume x in dom (Carrier F₂()) ; :: thesis: f . x in (Carrier F₂()) . x
then reconsider x' = x as Element of F₁() by PARTFUN1:def 4;
f . x' in the carrier of (F₂() . x') by A5;
hence f . x in (Carrier F₂()) . x by YELLOW_6:9; :: thesis: verum

end;

dom f = dom (Carrier F₂()) by A4, PARTFUN1:def 4;
then f in product (Carrier F₂()) by A6, CARD_3:18;
then reconsider f = f as Element of by WAYBEL18:def 3;
take f ; :: thesis: for i being Element of F₁() holds P₁[f . i,i]
let i be Element of F₁(); :: thesis: P₁[f . i,i]
thus P₁[f . i,i] by A5; :: thesis: verum