deffunc H₁( object ) -> set = f . (x,$1);
defpred S₁[ object ] means $1 in X-section ((dom f),x);

A1: 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;

A3: for d being object st S₁[d] holds
H₁(d) in Y by A1, PARTFUN1:4;
consider P being PartFunc of X2,Y such that
A4: ( ( for x being object holds
( x in dom P iff ( x in X2 & S₁[x] ) ) ) & ( for x being object st x in dom P holds
P . x = H₁(x) ) ) from PARTFUN1:sch 3(A3);
take P ; :: thesis: ( dom P = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
P . y = f . (x,y) ) )
A5: dom P c= X-section ((dom f),x) by A4;
X-section ((dom f),x) c= dom P by A4;
hence dom P = X-section ((dom f),x) by A5; :: thesis: for y being Element of X2 st [x,y] in dom f holds
P . y = f . (x,y)
thus for d being Element of X2 st [x,d] in dom f holds
P . d = f . (x,d) :: thesis: verum

proof

let d be Element of X2; :: thesis: ( [x,d] in dom f implies P . d = f . (x,d) )
assume [x,d] in dom f ; :: thesis: P . d = f . (x,d)
then d in { y where y is Element of X2 : [x,y] in dom f } ;
then d in X-section ((dom f),x) by MEASUR11:def 4;
hence P . d = f . (x,d) by A4; :: thesis: verum

end;