let P1, P2 be PartFunc of X2,Y; :: thesis:
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) ; :: thesis:

let d be object ; :: thesis:
assume d in X-section ((dom f),x) ; :: thesis:
then d in { y where y is Element of X2 : [x,y] in dom f } by MEASUR11:def 4;
then ex d1 being Element of X2 st
( d = d1 & [x,d1] in dom f ) ;
hence ( d in X2 & [x,d] in dom f ) ; :: thesis:

end;

let d be Element of X2; :: thesis:
assume d in dom P1 ; :: thesis:
then ( P1 . d = f . (x,d) & P2 . d = f . (x,d) ) by A1, A2, A4, A5;
hence P1 . d = P2 . d ; :: thesis:

end;