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