defpred S_{1}[ object , object ] means ( ( $1 in F_{1}() implies $2 = F_{5}() . $1 ) & ( $1 in F_{3}() \ F_{1}() implies $2 = F_{6}($1) ) );

A4: for x being object st x in F_{3}() holds

ex y being object st

( y in F_{4}() & S_{1}[x,y] )
_{3}(),F_{4}() such that

A9: for x being object st x in F_{3}() holds

S_{1}[x,h . x]
from FUNCT_2:sch 1(A4);

A10: dom F_{5}() = (dom h) /\ F_{1}()
_{1}() = F_{5}() & ( for x being set st x in F_{3}() \ F_{1}() holds

h . x = F_{6}(x) ) )

for x being object st x in dom F_{5}() holds

h . x = F_{5}() . x
_{1}() = F_{5}()
by A10, FUNCT_1:46; :: thesis: for x being set st x in F_{3}() \ F_{1}() holds

h . x = F_{6}(x)

thus for x being set st x in F_{3}() \ F_{1}() holds

h . x = F_{6}(x)
by A9; :: thesis: verum

A4: for x being object st x in F

ex y being object st

( y in F

proof

consider h being Function of F
let x be object ; :: thesis: ( x in F_{3}() implies ex y being object st

( y in F_{4}() & S_{1}[x,y] ) )

assume A5: x in F_{3}()
; :: thesis: ex y being object st

( y in F_{4}() & S_{1}[x,y] )

( y in F_{4}() & S_{1}[x,y] )
; :: thesis: verum

end;( y in F

assume A5: x in F

( y in F

now :: thesis: ex y being object st

( y in F_{4}() & S_{1}[x,y] )end;

hence
ex y being object st ( y in F

per cases
( x in F_{1}() or not x in F_{1}() )
;

end;

suppose A6:
x in F_{1}()
; :: thesis: ex y being object st

( y in F_{4}() & S_{1}[x,y] )

( y in F

then
x in dom F_{5}()
by A3, FUNCT_2:def 1;

then F_{5}() . x in rng F_{5}()
by FUNCT_1:def 3;

then A7: F_{5}() . x in F_{4}()
by A2;

not x in F_{3}() \ F_{1}()
by A6, XBOOLE_0:def 5;

hence ex y being object st

( y in F_{4}() & S_{1}[x,y] )
by A7; :: thesis: verum

end;then F

then A7: F

not x in F

hence ex y being object st

( y in F

suppose A8:
not x in F_{1}()
; :: thesis: ex y being object st

( y in F_{4}() & S_{1}[x,y] )

( y in F

then
x in F_{3}() \ F_{1}()
by A5, XBOOLE_0:def 5;

then F_{6}(x) in F_{4}()
by A1;

hence ex y being object st

( y in F_{4}() & S_{1}[x,y] )
by A8; :: thesis: verum

end;then F

hence ex y being object st

( y in F

( y in F

A9: for x being object st x in F

S

A10: dom F

proof
_{5}() = (dom h) /\ F_{1}()
; :: thesis: verum

end;

take
h
; :: thesis: ( h | Fnow :: thesis: dom F_{5}() = (dom h) /\ F_{1}()end;

hence
dom Fper cases
( F_{2}() is empty or not F_{2}() is empty )
;

end;

suppose A11:
not F_{2}() is empty
; :: thesis: dom F_{5}() = (dom h) /\ F_{1}()

then
not F_{4}() is empty
by A2;

then A12: dom h = F_{3}()
by FUNCT_2:def 1;

dom F_{5}() = F_{1}()
by A11, FUNCT_2:def 1;

hence dom F_{5}() = (dom h) /\ F_{1}()
by A2, A12, XBOOLE_1:28; :: thesis: verum

end;then A12: dom h = F

dom F

hence dom F

h . x = F

for x being object st x in dom F

h . x = F

proof

hence
h | F
let x be object ; :: thesis: ( x in dom F_{5}() implies h . x = F_{5}() . x )

assume x in dom F_{5}()
; :: thesis: h . x = F_{5}() . x

then x in F_{1}()
;

hence h . x = F_{5}() . x
by A2, A9; :: thesis: verum

end;assume x in dom F

then x in F

hence h . x = F

h . x = F

thus for x being set st x in F

h . x = F