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

A5: now :: thesis: for d being object st d in X-section ((dom f),x) holds
( d in X2 & [x,d] in dom f )

let d be object ; :: thesis: ( d in X-section ((dom f),x) implies ( d in X2 & [x,d] in dom f ) )
assume d in X-section ((dom f),x) ; :: thesis: ( d in X2 & [x,d] in dom f )
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: verum

end;

now :: thesis: for d being Element of X2 st d in dom P1 holds
P1 . d = P2 . d

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

end;

hence P1 = P2 by A1, A3, PARTFUN1:5; :: thesis: verum