defpred S_{1}[ set , set ] means for phi being Element of Funcs (F_{1}(),F_{2}()) st phi | F_{3}() = $1 holds

$2 = F_{5}(phi);

set Z = { F_{5}(phi9) where phi9 is Element of Funcs (F_{1}(),F_{2}()) : phi9 .: F_{3}() c= F_{4}() } ;

set x = the Element of { F_{5}(phi9) where phi9 is Element of Funcs (F_{1}(),F_{2}()) : phi9 .: F_{3}() c= F_{4}() } ;

A4: F_{2}() /\ F_{4}() c= F_{2}()
by XBOOLE_1:17;

assume A5: not { F_{5}(phi9) where phi9 is Element of Funcs (F_{1}(),F_{2}()) : phi9 .: F_{3}() c= F_{4}() } is finite
; :: thesis: contradiction

then { F_{5}(phi9) where phi9 is Element of Funcs (F_{1}(),F_{2}()) : phi9 .: F_{3}() c= F_{4}() } <> {}
;

then the Element of { F_{5}(phi9) where phi9 is Element of Funcs (F_{1}(),F_{2}()) : phi9 .: F_{3}() c= F_{4}() } in { F_{5}(phi9) where phi9 is Element of Funcs (F_{1}(),F_{2}()) : phi9 .: F_{3}() c= F_{4}() }
;

then consider phi being Element of Funcs (F_{1}(),F_{2}()) such that

the Element of { F_{5}(phi9) where phi9 is Element of Funcs (F_{1}(),F_{2}()) : phi9 .: F_{3}() c= F_{4}() } = F_{5}(phi)
and

A6: phi .: F_{3}() c= F_{4}()
;

_{1}() /\ F_{3}()),(F_{2}() /\ F_{4}())), Z = { F_{5}(phi9) where phi9 is Element of Funcs (F_{1}(),F_{2}()) : phi9 .: F_{3}() c= F_{4}() } as non empty set by A5, FUNCT_2:8;

A8: F_{2}() /\ F_{4}() c= F_{4}()
by XBOOLE_1:17;

A9: F_{1}() /\ F_{3}() c= F_{1}()
by XBOOLE_1:17;

A13: for f being Element of FF holds S_{1}[f,F . f]
from FUNCT_2:sch 3(A10);

Z c= F .: (Funcs ((F_{1}() /\ F_{3}()),(F_{2}() /\ F_{4}())))

$2 = F

set Z = { F

set x = the Element of { F

A4: F

assume A5: not { F

then { F

then the Element of { F

then consider phi being Element of Funcs (F

the Element of { F

A6: phi .: F

now :: thesis: ( F_{2}() /\ F_{4}() = {} implies F_{1}() /\ F_{3}() = {} )

then reconsider FF = Funcs ((Fassume
F_{2}() /\ F_{4}() = {}
; :: thesis: F_{1}() /\ F_{3}() = {}

then A7: phi .: F_{3}() = {}
by A6, XBOOLE_1:3, XBOOLE_1:19;

F_{1}() = dom phi
by FUNCT_2:def 1;

then F_{1}() misses F_{3}()
by A7, RELAT_1:118;

hence F_{1}() /\ F_{3}() = {}
; :: thesis: verum

end;then A7: phi .: F

F

then F

hence F

A8: F

A9: F

A10: now :: thesis: for f being Element of FF ex g being Element of Z st S_{1}[f,g]

consider F being Function of FF,Z such that let f be Element of FF; :: thesis: ex g being Element of Z st S_{1}[f,g]

consider phi being Element of Funcs (F_{1}(),F_{2}()) such that

A11: phi | (F_{1}() /\ F_{3}()) = f
by A9, A4, Th4;

A12: phi | F_{3}() = f
by A11, Th5;

ex g being Function st

( f = g & dom g = F_{1}() /\ F_{3}() & rng g c= F_{2}() /\ F_{4}() )
by FUNCT_2:def 2;

then rng (phi | F_{3}()) c= F_{4}()
by A8, A12;

then phi .: F_{3}() c= F_{4}()
by RELAT_1:115;

then F_{5}(phi) in Z
;

then reconsider g9 = F_{5}(phi) as Element of Z ;

take g = g9; :: thesis: S_{1}[f,g]

thus S_{1}[f,g]
by A3, A12; :: thesis: verum

end;consider phi being Element of Funcs (F

A11: phi | (F

A12: phi | F

ex g being Function st

( f = g & dom g = F

then rng (phi | F

then phi .: F

then F

then reconsider g9 = F

take g = g9; :: thesis: S

thus S

A13: for f being Element of FF holds S

Z c= F .: (Funcs ((F

proof

hence
contradiction
by A1, A2, A5; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Z or y in F .: (Funcs ((F_{1}() /\ F_{3}()),(F_{2}() /\ F_{4}()))) )

assume y in Z ; :: thesis: y in F .: (Funcs ((F_{1}() /\ F_{3}()),(F_{2}() /\ F_{4}())))

then consider phi being Element of Funcs (F_{1}(),F_{2}()) such that

A14: y = F_{5}(phi)
and

A15: phi .: F_{3}() c= F_{4}()
;

rng (phi | F_{3}()) c= F_{4}()
by A15, RELAT_1:115;

then A16: rng (phi | F_{3}()) c= F_{2}() /\ F_{4}()
by XBOOLE_1:19;

A17: dom (phi | F_{3}()) =
(dom phi) /\ F_{3}()
by RELAT_1:61

.= F_{1}() /\ F_{3}()
by FUNCT_2:def 1
;

then reconsider x = phi | F_{3}() as Element of Funcs ((F_{1}() /\ F_{3}()),(F_{2}() /\ F_{4}())) by A16, FUNCT_2:def 2;

phi | F_{3}() in Funcs ((F_{1}() /\ F_{3}()),(F_{2}() /\ F_{4}()))
by A17, A16, FUNCT_2:def 2;

then A18: x in dom F by FUNCT_2:def 1;

y = F . x by A13, A14;

hence y in F .: (Funcs ((F_{1}() /\ F_{3}()),(F_{2}() /\ F_{4}())))
by A18, FUNCT_1:def 6; :: thesis: verum

end;assume y in Z ; :: thesis: y in F .: (Funcs ((F

then consider phi being Element of Funcs (F

A14: y = F

A15: phi .: F

rng (phi | F

then A16: rng (phi | F

A17: dom (phi | F

.= F

then reconsider x = phi | F

phi | F

then A18: x in dom F by FUNCT_2:def 1;

y = F . x by A13, A14;

hence y in F .: (Funcs ((F