defpred S1[ object , object ] means ( P1[$2,$1] & ( for i9 being Element of F1() st $1 = i9 holds
$2 in the carrier of (F2() . i9) ) );
A2: for i being object st i in F1() holds
ex x being object st S1[i,x]
proof
let i be object ; :: thesis: ( i in F1() implies ex x being object st S1[i,x] )
assume i in F1() ; :: thesis: ex x being object st S1[i,x]
then reconsider i1 = i as Element of F1() ;
consider x being Element of (F2() . i1) such that
A3: P1[x,i1] by A1;
take x ; :: thesis: S1[i,x]
thus P1[x,i] by A3; :: thesis: for i9 being Element of F1() st i = i9 holds
x in the carrier of (F2() . i9)
let i9 be Element of F1(); :: thesis: ( i = i9 implies x in the carrier of (F2() . i9) )
assume i = i9 ; :: thesis: x in the carrier of (F2() . i9)
hence x in the carrier of (F2() . i9) ; :: thesis: verum
end;
consider f being Function such that
A4: dom f = F1() and
A5: for i being object st i in F1() holds
S1[i,f . i] from CLASSES1:sch 1(A2);
 A6: for x being object st x in dom (Carrier F2()) holds
f . x in (Carrier F2()) . x
proof
let x be object ; :: thesis: ( x in dom (Carrier F2()) implies f . x in (Carrier F2()) . x )
assume x in dom (Carrier F2()) ; :: thesis: f . x in (Carrier F2()) . x
then reconsider x9 = x as Element of F1() ;
f . x9 in the carrier of (F2() . x9) by A5;
hence f . x in (Carrier F2()) . x by YELLOW_6:2; :: thesis: verum
end;
dom f = dom (Carrier F2()) by A4, PARTFUN1:def 2;
then f in product (Carrier F2()) by A6, CARD_3:9;
then reconsider f = f as Element of (product F2()) by WAYBEL18:def 3;
take f ; :: thesis: for i being Element of F1() holds P1[f . i,i]
let i be Element of F1(); :: thesis: P1[f . i,i]
thus P1[f . i,i] by A5; :: thesis: verum