deffunc H1( object ) -> set = f . (x,$1);
defpred S1[ object ] means $1 in X-section ((dom f),x);
A3:
for d being object st S1[d] holds
H1(d) in Y
by A1, PARTFUN1:4;
consider P being PartFunc of X2,Y such that
A4:
( ( for x being object holds
( x in dom P iff ( x in X2 & S1[x] ) ) ) & ( for x being object st x in dom P holds
P . x = H1(x) ) )
from PARTFUN1:sch 3(A3);
take
P
; ( dom P = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
P . y = f . (x,y) ) )
A5:
dom P c= X-section ((dom f),x)
by A4;
X-section ((dom f),x) c= dom P
by A4;
hence
dom P = X-section ((dom f),x)
by A5; for y being Element of X2 st [x,y] in dom f holds
P . y = f . (x,y)
thus
for d being Element of X2 st [x,d] in dom f holds
P . d = f . (x,d)
verum