defpred S₁[ object , object ] means for f being Function of F₁(),F₂()
for h being Function of F₃(),F₄() st f = $1 & h = $2 holds
h | F₁() = f;
set F2 = { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ;
set F1 = { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } ;
A5: for f9 being object st f9 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } holds
ex g9 being object st
( g9 in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } & S₁[f9,g9] )

proof

let f9 be object ; :: thesis: ( f9 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } implies ex g9 being object st
( g9 in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } & S₁[f9,g9] ) )
assume f9 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } ; :: thesis: ex g9 being object st
( g9 in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } & S₁[f9,g9] )
then consider f being Function of F₁(),F₂() such that
A6: f = f9 and
A7: P₁[f,F₁(),F₂()] ;
consider h being Function of F₃(),F₄() such that
A8: ( h | F₁() = f & ( for x being set st x in F₃() \ F₁() holds
h . x = F₅(x) ) ) from STIRL2_1:sch 2(A1, A2, A3);
A9: S₁[f9,h] by A6, A8;
A10: rng f c= F₂() ;
P₁[h,F₃(),F₄()] by A4, A7, A8;
then h in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } by A8, A10;
hence ex g9 being object st
( g9 in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } & S₁[f9,g9] ) by A9; :: thesis: verum

end;

consider ff being Function of { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } , { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } such that
A11: for x being object st x in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } holds
S₁[x,ff . x] from FUNCT_2:sch 1(A5);
A12: ( F₄() is empty implies F₃() is empty ) by A1, A2, A3;

now :: thesis: card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

per cases ( F₄() is empty or not F₄() is empty ) ;

suppose A13: F₄() is empty ; :: thesis: card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

set Empty = {} ;
A14: { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } c= {{}}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } or x in {{}} )
assume x in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ; :: thesis: x in {{}}
then ex f being Function of F₃(),F₄() st
( f = x & P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) ;
then x = {} by A13;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

A15: { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } c= {{}}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } or x in {{}} )
assume x in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } ; :: thesis: x in {{}}
then ex f being Function of F₁(),F₂() st
( f = x & P₁[f,F₁(),F₂()] ) ;
then x = {} by A2, A13;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

per cases ( P₁[ {} , {} , {} ] or not P₁[ {} , {} , {} ] ) ;

suppose A16: P₁[ {} , {} , {} ] ; :: thesis: card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

A17: rng {} = {} ;
A18: F₂() is empty by A2, A13;
{} is Function of F₁(),F₂() by A3, A18, A17, FUNCT_2:1;
then {} in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } by A3, A16, A18;
then A19: { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = {{}} by A15, ZFMISC_1:33;
A20: rng {} = {} ;
reconsider Empty = {} as Function of F₃(),F₄() by A12, A13, A20, FUNCT_2:1;
A21: for x being set st x in F₃() \ F₁() holds
Empty . x = F₅(x) by A12;
rng (Empty | F₁()) c= F₂() ;
then {} in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } by A12, A13, A16, A21;
hence card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } by A14, A19, ZFMISC_1:33; :: thesis: verum

end;

suppose A22: P₁[ {} , {} , {} ] ; :: thesis: card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

A23: not {} in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] }

proof

assume {} in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } ; :: thesis: contradiction
then ex f being Function of F₁(),F₂() st
( f = {} & P₁[f,F₁(),F₂()] ) ;
hence contradiction by A2, A3, A13, A22; :: thesis: verum

end;

A24: ( { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } = {} or { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } = {{}} ) by A14, ZFMISC_1:33;
A25: not {} in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

proof

assume {} in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ; :: thesis: contradiction
then ex f being Function of F₃(),F₄() st
( f = {} & P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) ;
hence contradiction by A12, A13, A22; :: thesis: verum

end;

( { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = {} or { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = {{}} ) by A15, ZFMISC_1:33;
hence card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } by A23, A25, A24, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ; :: thesis: verum

end;

suppose A26: not F₄() is empty ; :: thesis: card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

now :: thesis: card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

per cases ( { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } is empty or not { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } is empty ) ;

suppose A27: { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } is empty ; :: thesis: card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

{ f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } is empty

proof

assume not { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } is empty ; :: thesis: contradiction
then consider x being object such that
A28: x in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } ;
consider f being Function of F₁(),F₂() such that
f = x and
A29: P₁[f,F₁(),F₂()] by A28;
A30: rng f c= F₂() ;
consider h being Function of F₃(),F₄() such that
A31: ( h | F₁() = f & ( for x being set st x in F₃() \ F₁() holds
h . x = F₅(x) ) ) from STIRL2_1:sch 2(A1, A2, A3);
P₁[h,F₃(),F₄()] by A4, A29, A31;
then h in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } by A31, A30;
hence contradiction by A27; :: thesis: verum

end;

hence card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } by A27; :: thesis: verum

end;

suppose A32: not { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } is empty ; :: thesis: card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) }

{ f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } c= rng ff

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } or y in rng ff )
assume y in { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ; :: thesis: y in rng ff
then consider f being Function of F₃(),F₄() such that
A33: f = y and
A34: P₁[f,F₃(),F₄()] and
A35: rng (f | F₁()) c= F₂() and
A36: for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ;
A37: dom (f | F₁()) = (dom f) /\ F₁() by RELAT_1:61;
dom f = F₃() by A26, FUNCT_2:def 1;
then A38: dom (f | F₁()) = F₁() by A2, A37, XBOOLE_1:28;
then reconsider h = f | F₁() as Function of F₁(),(rng (f | F₁())) by FUNCT_2:1;
( rng (f | F₁()) is empty implies F₁() is empty ) by A38, RELAT_1:42;
then reconsider h = h as Function of F₁(),F₂() by A35, FUNCT_2:6;
P₁[f | F₁(),F₁(),F₂()] by A4, A34, A36;
then A39: h in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } ;
A40: dom ff = { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } 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₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ;
then consider ffh being Function of F₃(),F₄() such that
A41: ffh = ff . h and
P₁[ffh,F₃(),F₄()] and
rng (ffh | F₁()) c= F₂() and
A42: for x being set st x in F₃() \ F₁() holds
ffh . x = F₅(x) ;

now :: thesis: for x being object st x in F₃() holds
ffh . x = f . x

let x be object ; :: thesis: ( x in F₃() implies ffh . x = f . x )
assume A43: x in F₃() ; :: thesis: ffh . x = f . x

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

per cases ( x in F₁() or not x in F₁() ) ;

suppose x in F₁() ; :: thesis: ffh . x = f . x

then A44: x in dom h by A3, FUNCT_2:def 1;
ffh | F₁() = h by A11, A39, A41;
then h . x = ffh . x by A44, FUNCT_1:47;
hence ffh . x = f . x by A44, FUNCT_1:47; :: thesis: verum

end;

suppose not x in F₁() ; :: thesis: ffh . x = f . x

then A45: x in F₃() \ F₁() by A43, XBOOLE_0:def 5;
then ffh . x = F₅(x) by A42;
hence ffh . x = f . x by A36, A45; :: thesis: verum

end;

end;

end;

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

end;

then ffh = f by FUNCT_2:12;
hence y in rng ff by A33, A39, A40, A41, FUNCT_1:def 3; :: thesis: verum

end;

then A46: rng ff = { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ;
for x1, x2 being object st x1 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } & x2 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } & ff . x1 = ff . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } & x2 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } & ff . x1 = ff . x2 implies x1 = x2 )
assume that
A47: x1 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } and
A48: x2 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } and
A49: ff . x1 = ff . x2 ; :: thesis: x1 = x2
A50: ex f2 being Function of F₁(),F₂() st
( x2 = f2 & P₁[f2,F₁(),F₂()] ) by A48;
dom ff = { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } 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₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ;
then consider F1 being Function of F₃(),F₄() such that
A51: ff . x1 = F1 and
P₁[F1,F₃(),F₄()] and
rng (F1 | F₁()) c= F₂() and
for x being set st x in F₃() \ F₁() holds
F1 . x = F₅(x) ;
consider f1 being Function of F₁(),F₂() such that
A52: x1 = f1 and
P₁[f1,F₁(),F₂()] by A47;
F1 | F₁() = f1 by A11, A47, A52, A51;
hence x1 = x2 by A11, A48, A49, A52, A50, A51; :: thesis: verum

end;

then A53: ff is one-to-one by A32, FUNCT_2:19;
dom ff = { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } by A32, FUNCT_2:def 1;
then { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } , { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } are_equipotent by A46, A53, WELLORD2:def 4;
hence card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } by CARD_1:5; :: thesis: verum

end;

end;

end;

hence card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ; :: thesis: verum

end;

end;

end;

hence card { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } = card { f where f is Function of F₃(),F₄() : ( P₁[f,F₃(),F₄()] & rng (f | F₁()) c= F₂() & ( for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ) ) } ; :: thesis: verum