defpred S_{1}[ object , object ] means for f being Function of F_{1}(),F_{2}()

for h being Function of F_{3}(),F_{4}() st f = $1 & h = $2 holds

h | F_{1}() = f;

set F2 = { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } ;

set F1 = { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } ;

A5: for f9 being object st f9 in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } holds

ex g9 being object st

( g9 in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } & S_{1}[f9,g9] )
_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } , { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } such that

A11: for x being object st x in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } holds

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

A12: ( F_{4}() is empty implies F_{3}() is empty )
by A1, A2, A3;

_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
; :: thesis: verum

for h being Function of F

h | F

set F2 = { f where f is Function of F

f . x = F

set F1 = { f where f is Function of F

A5: for f9 being object st f9 in { f where f is Function of F

ex g9 being object st

( g9 in { f where f is Function of F

f . x = F

proof

consider ff being Function of { f where f is Function of F
let f9 be object ; :: thesis: ( f9 in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } implies ex g9 being object st

( g9 in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } & S_{1}[f9,g9] ) )

assume f9 in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
; :: thesis: ex g9 being object st

( g9 in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } & S_{1}[f9,g9] )

then consider f being Function of F_{1}(),F_{2}() such that

A6: f = f9 and

A7: P_{1}[f,F_{1}(),F_{2}()]
;

consider h being Function of F_{3}(),F_{4}() such that

A8: ( h | F_{1}() = f & ( for x being set st x in F_{3}() \ F_{1}() holds

h . x = F_{5}(x) ) )
from STIRL2_1:sch 2(A1, A2, A3);

A9: S_{1}[f9,h]
by A6, A8;

A10: rng f c= F_{2}()
;

P_{1}[h,F_{3}(),F_{4}()]
by A4, A7, A8;

then h in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
by A8, A10;

hence ex g9 being object st

( g9 in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } & S_{1}[f9,g9] )
by A9; :: thesis: verum

end;( g9 in { f where f is Function of F

f . x = F

assume f9 in { f where f is Function of F

( g9 in { f where f is Function of F

f . x = F

then consider f being Function of F

A6: f = f9 and

A7: P

consider h being Function of F

A8: ( h | F

h . x = F

A9: S

A10: rng f c= F

P

then h in { f where f is Function of F

f . x = F

hence ex g9 being object st

( g9 in { f where f is Function of F

f . x = F

f . x = F

A11: for x being object st x in { f where f is Function of F

S

A12: ( F

now :: thesis: card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } end;

hence
card { f where f is Function of Ff . x = F

per cases
( F_{4}() is empty or not F_{4}() is empty )
;

end;

suppose A13:
F_{4}() is empty
; :: thesis: card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }

f . x = F

set Empty = {} ;

A14: { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } c= {{}}
_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } c= {{}}
_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
; :: thesis: verum

end;A14: { f where f is Function of F

f . x = F

proof

A15:
{ f where f is Function of F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } or x in {{}} )

assume x in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
; :: thesis: x in {{}}

then ex f being Function of F_{3}(),F_{4}() st

( f = x & P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) )
;

then x = {} by A13;

hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;f . x = F

assume x in { f where f is Function of F

f . x = F

then ex f being Function of F

( f = x & P

f . x = F

then x = {} by A13;

hence x in {{}} by TARSKI:def 1; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } or x in {{}} )

assume x in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
; :: thesis: x in {{}}

then ex f being Function of F_{1}(),F_{2}() st

( f = x & P_{1}[f,F_{1}(),F_{2}()] )
;

then x = {} by A2, A13;

hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;assume x in { f where f is Function of F

then ex f being Function of F

( f = x & P

then x = {} by A2, A13;

hence x in {{}} by TARSKI:def 1; :: thesis: verum

now :: thesis: card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } end;

hence
card { f where f is Function of Ff . x = F

per cases
( P_{1}[ {} , {} , {} ] or not P_{1}[ {} , {} , {} ] )
;

end;

suppose A16:
P_{1}[ {} , {} , {} ]
; :: thesis: card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }

f . x = F

A17:
rng {} = {}
;

A18: F_{2}() is empty
by A2, A13;

{} is Function of F_{1}(),F_{2}()
by A3, A18, A17, FUNCT_2:1;

then {} in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
by A3, A16, A18;

then A19: { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = {{}}
by A15, ZFMISC_1:33;

A20: rng {} = {} ;

reconsider Empty = {} as Function of F_{3}(),F_{4}() by A12, A13, A20, FUNCT_2:1;

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

Empty . x = F_{5}(x)
by A12;

rng (Empty | F_{1}()) c= F_{2}()
;

then {} in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
by A12, A13, A16, A21;

hence card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
by A14, A19, ZFMISC_1:33; :: thesis: verum

end;A18: F

{} is Function of F

then {} in { f where f is Function of F

then A19: { f where f is Function of F

A20: rng {} = {} ;

reconsider Empty = {} as Function of F

A21: for x being set st x in F

Empty . x = F

rng (Empty | F

then {} in { f where f is Function of F

f . x = F

hence card { f where f is Function of F

f . x = F

suppose A22:
P_{1}[ {} , {} , {} ]
; :: thesis: card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }

f . x = F

A23:
not {} in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } = {} or { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } = {{}} )
by A14, ZFMISC_1:33;

A25: not {} in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = {} or { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = {{}} )
by A15, ZFMISC_1:33;

hence card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
by A23, A25, A24, TARSKI:def 1; :: thesis: verum

end;proof

A24:
( { f where f is Function of F
assume
{} in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
; :: thesis: contradiction

then ex f being Function of F_{1}(),F_{2}() st

( f = {} & P_{1}[f,F_{1}(),F_{2}()] )
;

hence contradiction by A2, A3, A13, A22; :: thesis: verum

end;then ex f being Function of F

( f = {} & P

hence contradiction by A2, A3, A13, A22; :: thesis: verum

f . x = F

f . x = F

A25: not {} in { f where f is Function of F

f . x = F

proof

( { f where f is Function of F
assume
{} in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
; :: thesis: contradiction

then ex f being Function of F_{3}(),F_{4}() st

( f = {} & P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) )
;

hence contradiction by A12, A13, A22; :: thesis: verum

end;f . x = F

then ex f being Function of F

( f = {} & P

f . x = F

hence contradiction by A12, A13, A22; :: thesis: verum

hence card { f where f is Function of F

f . x = F

f . x = F

suppose A26:
not F_{4}() is empty
; :: thesis: card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }

_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
; :: thesis: verum

end;

f . x = F

now :: thesis: card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } end;

hence
card { f where f is Function of Ff . x = F

per cases
( { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } is empty or not { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } is empty )
;

end;

f . x = F

f . x = F

suppose A27:
{ f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } is empty
; :: thesis: card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }

f . x = F

f . x = F

{ f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } is empty
_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
by A27; :: thesis: verum

end;proof

hence
card { f where f is Function of F
assume
not { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } is empty
; :: thesis: contradiction

then consider x being object such that

A28: x in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
;

consider f being Function of F_{1}(),F_{2}() such that

f = x and

A29: P_{1}[f,F_{1}(),F_{2}()]
by A28;

A30: rng f c= F_{2}()
;

consider h being Function of F_{3}(),F_{4}() such that

A31: ( h | F_{1}() = f & ( for x being set st x in F_{3}() \ F_{1}() holds

h . x = F_{5}(x) ) )
from STIRL2_1:sch 2(A1, A2, A3);

P_{1}[h,F_{3}(),F_{4}()]
by A4, A29, A31;

then h in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
by A31, A30;

hence contradiction by A27; :: thesis: verum

end;then consider x being object such that

A28: x in { f where f is Function of F

consider f being Function of F

f = x and

A29: P

A30: rng f c= F

consider h being Function of F

A31: ( h | F

h . x = F

P

then h in { f where f is Function of F

f . x = F

hence contradiction by A27; :: thesis: verum

f . x = F

suppose A32:
not { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } is empty
; :: thesis: card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }

f . x = F

f . x = F

{ f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } c= rng ff
_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
;

for x1, x2 being object st x1 in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } & x2 in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } & ff . x1 = ff . x2 holds

x1 = x2

dom ff = { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
by A32, FUNCT_2:def 1;

then { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } , { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } are_equipotent
by A46, A53, WELLORD2:def 4;

hence card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
by CARD_1:5; :: thesis: verum

end;f . x = F

proof

then A46:
rng ff = { f where f is Function of F
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) } or y in rng ff )

assume y in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
; :: thesis: y in rng ff

then consider f being Function of F_{3}(),F_{4}() such that

A33: f = y and

A34: P_{1}[f,F_{3}(),F_{4}()]
and

A35: rng (f | F_{1}()) c= F_{2}()
and

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

f . x = F_{5}(x)
;

A37: dom (f | F_{1}()) = (dom f) /\ F_{1}()
by RELAT_1:61;

dom f = F_{3}()
by A26, FUNCT_2:def 1;

then A38: dom (f | F_{1}()) = F_{1}()
by A2, A37, XBOOLE_1:28;

then reconsider h = f | F_{1}() as Function of F_{1}(),(rng (f | F_{1}())) by FUNCT_2:1;

( rng (f | F_{1}()) is empty implies F_{1}() is empty )
by A38, RELAT_1:42;

then reconsider h = h as Function of F_{1}(),F_{2}() by A35, FUNCT_2:6;

P_{1}[f | F_{1}(),F_{1}(),F_{2}()]
by A4, A34, A36;

then A39: h in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
;

A40: dom ff = { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
by A32, FUNCT_2:def 1;

then ff . h in rng ff by A39, FUNCT_1:def 3;

then ff . h in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
;

then consider ffh being Function of F_{3}(),F_{4}() such that

A41: ffh = ff . h and

P_{1}[ffh,F_{3}(),F_{4}()]
and

rng (ffh | F_{1}()) c= F_{2}()
and

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

ffh . x = F_{5}(x)
;

hence y in rng ff by A33, A39, A40, A41, FUNCT_1:def 3; :: thesis: verum

end;f . x = F

assume y in { f where f is Function of F

f . x = F

then consider f being Function of F

A33: f = y and

A34: P

A35: rng (f | F

A36: for x being set st x in F

f . x = F

A37: dom (f | F

dom f = F

then A38: dom (f | F

then reconsider h = f | F

( rng (f | F

then reconsider h = h as Function of F

P

then A39: h in { f where f is Function of F

A40: dom ff = { f where f is Function of F

then ff . h in rng ff by A39, FUNCT_1:def 3;

then ff . h in { f where f is Function of F

f . x = F

then consider ffh being Function of F

A41: ffh = ff . h and

P

rng (ffh | F

A42: for x being set st x in F

ffh . x = F

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

ffh . x = f . x

then
ffh = f
by FUNCT_2:12;ffh . x = f . x

let x be object ; :: thesis: ( x in F_{3}() implies ffh . x = f . x )

assume A43: x in F_{3}()
; :: thesis: ffh . x = f . x

end;assume A43: x in F

now :: thesis: ffh . x = f . x

hence
ffh . x = f . x
; :: thesis: verumend;

hence y in rng ff by A33, A39, A40, A41, FUNCT_1:def 3; :: thesis: verum

f . x = F

for x1, x2 being object st x1 in { f where f is Function of F

x1 = x2

proof

then A53:
ff is one-to-one
by A32, FUNCT_2:19;
let x1, x2 be object ; :: thesis: ( x1 in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } & x2 in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } & ff . x1 = ff . x2 implies x1 = x2 )

assume that

A47: x1 in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
and

A48: x2 in { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
and

A49: ff . x1 = ff . x2 ; :: thesis: x1 = x2

A50: ex f2 being Function of F_{1}(),F_{2}() st

( x2 = f2 & P_{1}[f2,F_{1}(),F_{2}()] )
by A48;

dom ff = { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] }
by A32, FUNCT_2:def 1;

then ff . x1 in rng ff by A47, FUNCT_1:def 3;

then ff . x1 in { f where f is Function of F_{3}(),F_{4}() : ( P_{1}[f,F_{3}(),F_{4}()] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in F_{3}() \ F_{1}() holds

f . x = F_{5}(x) ) ) }
;

then consider F1 being Function of F_{3}(),F_{4}() such that

A51: ff . x1 = F1 and

P_{1}[F1,F_{3}(),F_{4}()]
and

rng (F1 | F_{1}()) c= F_{2}()
and

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

F1 . x = F_{5}(x)
;

consider f1 being Function of F_{1}(),F_{2}() such that

A52: x1 = f1 and

P_{1}[f1,F_{1}(),F_{2}()]
by A47;

F1 | F_{1}() = f1
by A11, A47, A52, A51;

hence x1 = x2 by A11, A48, A49, A52, A50, A51; :: thesis: verum

end;assume that

A47: x1 in { f where f is Function of F

A48: x2 in { f where f is Function of F

A49: ff . x1 = ff . x2 ; :: thesis: x1 = x2

A50: ex f2 being Function of F

( x2 = f2 & P

dom ff = { f where f is Function of F

then ff . x1 in rng ff by A47, FUNCT_1:def 3;

then ff . x1 in { f where f is Function of F

f . x = F

then consider F1 being Function of F

A51: ff . x1 = F1 and

P

rng (F1 | F

for x being set st x in F

F1 . x = F

consider f1 being Function of F

A52: x1 = f1 and

P

F1 | F

hence x1 = x2 by A11, A48, A49, A52, A50, A51; :: thesis: verum

dom ff = { f where f is Function of F

then { f where f is Function of F

f . x = F

hence card { f where f is Function of F

f . x = F

f . x = F

f . x = F