defpred S1[ object , object ] means $2 in F2($1);
A2:
now for e being object st e in F1() holds
ex fe being object st S1[e,fe]let e be
object ;
( e in F1() implies ex fe being object st S1[e,fe] )set fe = the
Element of
F2(
e);
assume A3:
e in F1()
;
ex fe being object st S1[e,fe]reconsider fe = the
Element of
F2(
e) as
object ;
take fe =
fe;
S1[e,fe]
F2(
e)
<> {}
by A1, A3;
hence
S1[
e,
fe]
;
verum end;
consider f being Function such that
A4:
dom f = F1()
and
A5:
for e being object st e in F1() holds
S1[e,f . e]
from CLASSES1:sch 1(A2);
reconsider f = f as ManySortedSet of F1() by A4, PARTFUN1:def 2, RELAT_1:def 18;
take
f
; for e being object st e in F1() holds
f . e in F2(e)
thus
for e being object st e in F1() holds
f . e in F2(e)
by A5; verum