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

proof

let x, y, z be object ; :: 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 and
A3: S₁[x,g1] ; :: thesis: ( not S₂[x,z] or y = z )
given g2 being Function such that A4: z = g2 and
A5: S₁[x,g2] ; :: thesis: y = z

now :: thesis: for t being object st t in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) holds
g1 . t = g2 . t

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

end;

hence y = z by A2, A3, A4, A5, FUNCT_1:2; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in proj1 (dom f) implies ex y being object st S₂[x,y] )
assume x in proj1 (dom f) ; :: thesis: ex y being object st S₂[x,y]
deffunc H₁( object ) -> set = f . [x,$1];
consider g being Function such that
A8: ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being object 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 A = y; :: thesis: S₂[x,A]
take B = g; :: thesis: ( A = B & S₁[x,B] )
thus ( A = B & S₁[x,B] ) by A8; :: thesis: verum

end;

ex g being Function st
( dom g = proj1 (dom f) & ( for x being object st x in proj1 (dom f) holds
S₂[x,g . x] ) ) from FUNCT_1:sch 2(A1, A7);
hence ex b₁ being Function st
( dom b₁ = proj1 (dom f) & ( for x being object 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 object st y in dom g holds
g . y = f . (x,y) ) ) ) ) ; :: thesis: verum