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

A5: now :: thesis: for c being object st c in Y-section ((dom f),y) holds
( c in X1 & [c,y] in dom f )

let c be object ; :: thesis: ( c in Y-section ((dom f),y) implies ( c in X1 & [c,y] in dom f ) )
assume c in Y-section ((dom f),y) ; :: thesis: ( c in X1 & [c,y] in dom f )
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: verum

end;

now :: thesis: for c being Element of X1 st c in dom P1 holds
P1 . c = P2 . c

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

end;

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