consider f being Function such that
A1:
dom f = F1()
and
A2:
for x being object st x in F1() holds
for y being object holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) )
from CARD_3:sch 2();
take
f
; ( dom f = F1() & ( for x being set st x in F1() holds
for y being set holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) ) ) )
thus
( dom f = F1() & ( for x being set st x in F1() holds
for y being set holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) ) ) )
by A1, A2; verum