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

proof

let x be object ; :: thesis: ( x in Y implies ex y being object st S₁[x,y] )
assume x in Y ; :: thesis: ex y being object 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 object 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 object st x in Y holds
S₁[x,F . x] ) ) from FUNCT_1:sch 2(A25, A24);
take F ; :: thesis: ( ( for t being object holds
( t in dom F iff ex x being object ex g being Function ex y being object st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being object
for g being Function st x in dom F & g = f . (x `1) holds
F . x = g . (x `2) ) )
thus for t being object holds
( t in dom F iff ex x being object ex g being Function ex y being object st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) :: thesis: for x being object
for g being Function st x in dom F & g = f . (x `1) holds
F . x = g . (x `2)

proof

let t be object ; :: thesis: ( t in dom F iff ex x being object ex g being Function ex y being object st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) )
thus ( t in dom F implies ex x being object ex g being Function ex y being object st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) :: thesis: ( ex x being object ex g being Function ex y being object 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 object ex g being Function ex y being object 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 object st
( t = [x,y] & x in dom f & g = f . x & y in dom g )
t in [:X,(union (rng g)):] by A23, A26, A27;
then A28: x in X by MCART_1:10;
then reconsider h = f . x as Function by A21;
take h ; :: thesis: ex y being object 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, MCART_1:21; :: thesis: verum

end;

given x being object , h being Function, y being object such that A29: t = [x,y] and
A30: x in dom f and
A31: h = f . x and
A32: y in dom h ; :: thesis: t in dom F
A33: x in X by A21, A30, A31;
then h in f .: X by A30, A31, 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 A34: t in [:X,(union (rng g)):] by A29, A32, A33, ZFMISC_1:87;
for g1 being Function st g1 = f . (t `1) holds
t `2 in dom g1 by A29, A31, A32;
hence t in dom F by A23, A26, A34; :: thesis: verum

end;

let x be object ; :: 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
A35: x in dom F and
A36: 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, A35;
hence F . x = h . (x `2) by A36; :: thesis: verum