defpred S₁[ set , set ] means ex g being Function st
( g = f . ($1 `1) & $2 = g . ($1 `2) );
deffunc H₁( Function) -> set = dom $1;
defpred S₂[ set ] means f . $1 is Function;
consider X being set such that
A21: for x being set holds
( x in X iff ( x in dom f & S₂[x] ) ) from XBOOLE_0:sch 1();
defpred S₃[ set ] means for g1 being Function st g1 = f . ($1 `1) holds
$1 `2 in dom g1;
consider g being Function such that
A22: ( dom g = f .: X & ( for g1 being Function st g1 in f .: X holds
g . g1 = H₁(g1) ) ) from FUNCT_5:sch 1();
consider Y being set such that
A23: for x being set holds
( x in Y iff ( x in [:X,(union (rng g)):] & S₃[x] ) ) from XBOOLE_0:sch 1();
A24: for x being set st x in Y holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in Y implies ex y being set st S₁[x,y] )
assume x in Y ; :: thesis: ex y being set st S₁[x,y]
then x in [:X,(union (rng g)):] by A23;
then x `1 in X by MCART_1:10;
then reconsider h = f . (x `1) as Function by A21;
take h . (x `2) ; :: thesis: S<sub>1</sub>[x,h . (x `2)]
take h ; :: thesis: ( h = f . (x `1) & h . (x `2) = h . (x `2) )
thus ( h = f . (x `1) & h . (x `2) = h . (x `2) ) ; :: thesis: verum

end;

A25: for x, x1, x2 being set st x in Y & S₁[x,x1] & S₁[x,x2] holds
x1 = x2 ;
consider F being Function such that
A26: ( dom F = Y & ( for x being set st x in Y holds
S₁[x,F . x] ) ) from FUNCT_1:sch 2(A25, A24);
take F ; :: thesis: ( ( for t being set holds
( t in dom F iff ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set
for g being Function st x in dom F & g = f . (x `1) holds
F . x = g . (x `2) ) )
thus for t being set holds
( t in dom F iff ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) :: thesis: for x being set
for g being Function st x in dom F & g = f . (x `1) holds
F . x = g . (x `2)

proof

let t be set ; :: thesis: ( t in dom F iff ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) )
thus ( t in dom F implies ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) :: thesis: ( ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) implies t in dom F )

proof

assume A27: t in dom F ; :: thesis: ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g )
take x = t `1 ; :: thesis: ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g )
A28: t in [:X,(union (rng g)):] by A23, A26, A27;
then A29: x in X by MCART_1:10;
then reconsider h = f . x as Function by A21;
take h ; :: thesis: ex y being set st
( t = [x,y] & x in dom f & h = f . x & y in dom h )
take t `2 ; :: thesis: ( t = [x,(t `2)] & x in dom f & h = f . x & t `2 in dom h )
thus ( t = [x,(t `2)] & x in dom f & h = f . x & t `2 in dom h ) by A21, A23, A26, A27, A28, A29, MCART_1:21; :: thesis: verum

end;

given x being set , h being Function, y being set such that A30: t = [x,y] and
A31: x in dom f and
A32: h = f . x and
A33: y in dom h ; :: thesis: t in dom F
A34: x in X by A21, A31, A32;
then h in f .: X by A31, A32, FUNCT_1:def 6;
then ( g . h = dom h & g . h in rng g ) by A22, FUNCT_1:def 3;
then dom h c= union (rng g) by ZFMISC_1:74;
then A35: t in [:X,(union (rng g)):] by A30, A33, A34, ZFMISC_1:87;
t `1 = x by A30, MCART_1:7;
then for g1 being Function st g1 = f . (t `1) holds
t `2 in dom g1 by A30, A32, A33, MCART_1:7;
hence t in dom F by A23, A26, A35; :: thesis: verum

end;

let x be set ; :: thesis: for g being Function st x in dom F & g = f . (x `1) holds
F . x = g . (x `2)
let h be Function; :: thesis: ( x in dom F & h = f . (x `1) implies F . x = h . (x `2) )
assume that
A36: x in dom F and
A37: h = f . (x `1) ; :: thesis: F . x = h . (x `2)
ex g being Function st
( g = f . (x `1) & F . x = g . (x `2) ) by A26, A36;
hence F . x = h . (x `2) by A37; :: thesis: verum