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

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

A3: for c being object st S₁[c] holds
H₁(c) in Y by A1, PARTFUN1:4;
consider P being PartFunc of X1,Y such that
A4: ( ( for x being object holds
( x in dom P iff ( x in X1 & 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 = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds
P . x = f . (x,y) ) )
A5: dom P c= Y-section ((dom f),y) by A4;
Y-section ((dom f),y) c= dom P by A4;
hence dom P = Y-section ((dom f),y) by A5; :: thesis: for x being Element of X1 st [x,y] in dom f holds
P . x = f . (x,y)
thus for c being Element of X1 st [c,y] in dom f holds
P . c = f . (c,y) :: thesis: verum

proof

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

end;