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

let c be object ; :: thesis:
assume c in Y-section ((dom f),y) ; :: thesis:
then c in { x where x is Element of X1 : [x,y] in dom f } by MEASUR11:def 5;
then ex c1 being Element of X1 st
( c = c1 & [c1,y] in dom f ) ;
hence ( c in X1 & [c,y] in dom f ) ; :: thesis:

end;

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

end;