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

proof

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

end;

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

proof

let x be object ; :: 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 x9 = x as Element of F₁() ;
f . x9 in the carrier of (F₂() . x9) by A5;
hence f . x in (Carrier F₂()) . x by YELLOW_6:2; :: thesis: verum

end;

dom f = dom (Carrier F₂()) by A4, PARTFUN1:def 2;
then f in product (Carrier F₂()) by A6, CARD_3:9;
then reconsider f = f as Element of (product F₂()) 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