defpred S₁[ set , Function] means ( dom $2 = proj2 ((dom f) /\ [:{$1},(proj2 (dom f)):]) & ( for y being set st y in dom $2 holds
$2 . y = f . $1,y ) );
defpred S₂[ set , set ] means ex g being Function st
( $2 = g & S₁[$1,g] );
A1: for x, y, z being set st x in proj1 (dom f) & S₂[x,y] & S₂[x,z] holds
y = z

proof

let x, y, z be set ; :: thesis: ( x in proj1 (dom f) & S₂[x,y] & S₂[x,z] implies y = z )
assume x in proj1 (dom f) ; :: thesis: ( not S₂[x,y] or not S₂[x,z] or y = z )
given g1 being Function such that A2: ( y = g1 & S₁[x,g1] ) ; :: thesis: ( not S₂[x,z] or y = z )
given g2 being Function such that A3: ( z = g2 & S₁[x,g2] ) ; :: thesis: y = z

now

let t be set ; :: thesis: ( t in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) implies g1 . t = g2 . t )
assume t in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) ; :: thesis: g1 . t = g2 . t
then ( g1 . t = f . x,t & g2 . t = f . x,t ) by A2, A3;
hence g1 . t = g2 . t ; :: thesis: verum

end;

hence y = z by A2, A3, FUNCT_1:9; :: thesis: verum

end;

A4: for x being set st x in proj1 (dom f) holds
ex y being set st S₂[x,y]

proof

let x be set ; :: thesis: ( x in proj1 (dom f) implies ex y being set st S₂[x,y] )
assume x in proj1 (dom f) ; :: thesis: ex y being set st S₂[x,y]
deffunc H₁( set ) -> set = f . [x,$1];
consider g being Function such that
A5: ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) holds
g . y = H₁(y) ) ) from FUNCT_1:sch 3();
reconsider y = g as set ;
take y ; :: thesis: S₂[x,y]
take g ; :: thesis: ( y = g & S₁[x,g] )
thus ( y = g & S₁[x,g] ) by A5; :: thesis: verum

end;

ex g being Function st
( dom g = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds
S₂[x,g . x] ) ) from FUNCT_1:sch 2(A1, A4);
hence ex b₁ being Function st
( dom b₁ = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds
ex g being Function st
( b₁ . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds
g . y = f . x,y ) ) ) ) ; :: thesis: verum