defpred S₁[ set , set ] 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 set st f9 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } holds
ex g9 being set 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 set ; :: thesis: ( f9 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } implies ex g9 being set 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 set 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 set 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 set 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 )

proof

assume A13: F₄() is empty ; :: thesis: F₃() is empty
assume not F₃() is empty ; :: thesis: contradiction
then ex x being set st x in F₃() by XBOOLE_0:def 1;
hence contradiction by A1, A2, A3, A13; :: thesis: verum

end;

now

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

suppose A14: 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 = {} ;
A15: { 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 set ; :: 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 A14;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

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

proof

let x be set ; :: 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, A14;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

now

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

suppose A17: 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) ) ) }

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

end;

suppose A23: 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) ) ) }

A24: 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, A14, A23; :: thesis: verum

end;

A25: ( { 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 A15, ZFMISC_1:33;
A26: 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, A14, A23; :: 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 A16, 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 A24, A26, A25, 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 A27: 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

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 A28: { 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 set such that
A29: x in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } by XBOOLE_0:def 1;
consider f being Function of F₁(),F₂() such that
f = x and
A30: P₁[f,F₁(),F₂()] by A29;
A31: rng f c= F₂() ;
consider h being Function of F₃(),F₄() such that
A32: ( 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, A30, A32;
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 A32, A31;
hence contradiction by A28; :: 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 A28; :: thesis: verum

end;

suppose A33: 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 set ; :: 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
A34: f = y and
A35: P₁[f,F₃(),F₄()] and
A36: rng (f | F₁()) c= F₂() and
A37: for x being set st x in F₃() \ F₁() holds
f . x = F₅(x) ;
A38: dom (f | F₁()) = (dom f) /\ F₁() by RELAT_1:61;
dom f = F₃() by A27, FUNCT_2:def 1;
then A39: dom (f | F₁()) = F₁() by A2, A38, 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 A39, RELAT_1:42;
then reconsider h = h as Function of F₁(),F₂() by A36, FUNCT_2:6;
P₁[f | F₁(),F₁(),F₂()] by A4, A35, A37;
then A40: h in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } ;
A41: dom ff = { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } by A33, FUNCT_2:def 1;
then ff . h in rng ff by A40, 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
A42: ffh = ff . h and
P₁[ffh,F₃(),F₄()] and
rng (ffh | F₁()) c= F₂() and
A43: for x being set st x in F₃() \ F₁() holds
ffh . x = F₅(x) ;

now

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

now

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

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

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

end;

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

then A46: x in F₃() \ F₁() by A44, XBOOLE_0:def 5;
then ffh . x = F₅(x) by A43;
hence ffh . x = f . x by A37, A46; :: 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 A34, A40, A41, A42, FUNCT_1:def 3; :: thesis: verum

end;

then A47: 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) ) ) } by XBOOLE_0:def 10;
for x1, x2 being set 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 set ; :: 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
A48: x1 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } and
A49: x2 in { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } and
A50: ff . x1 = ff . x2 ; :: thesis: x1 = x2
A51: ex f2 being Function of F₁(),F₂() st
( x2 = f2 & P₁[f2,F₁(),F₂()] ) by A49;
dom ff = { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } by A33, FUNCT_2:def 1;
then ff . x1 in rng ff by A48, 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
A52: 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
A53: x1 = f1 and
P₁[f1,F₁(),F₂()] by A48;
F1 | F₁() = f1 by A11, A48, A53, A52;
hence x1 = x2 by A11, A49, A50, A53, A51, A52; :: thesis: verum

end;

then A54: ff is one-to-one by A33, FUNCT_2:19;
dom ff = { f where f is Function of F₁(),F₂() : P₁[f,F₁(),F₂()] } by A33, 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 A47, A54, 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