let P1, P2 be PartFunc of X2,Y; ( dom P1 = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
P1 . y = f . (x,y) ) & dom P2 = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
P2 . y = f . (x,y) ) implies P1 = P2 )
assume that
A1:
dom P1 = X-section ((dom f),x)
and
A2:
for d being Element of X2 st [x,d] in dom f holds
P1 . d = f . (x,d)
and
A3:
dom P2 = X-section ((dom f),x)
and
A4:
for d being Element of X2 st [x,d] in dom f holds
P2 . d = f . (x,d)
; P1 = P2
hence
P1 = P2
by A1, A3, PARTFUN1:5; verum