let k, n be Nat; :: thesis: card { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }
set F1 = { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } ;
set F2 = { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } ;
now :: thesis: card { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }
per cases not ( not ( k = 0 & n <> 0 ) & k = 0 & not n = 0 ) ;
suppose A1: ( k = 0 & n <> 0 ) ; :: thesis: card { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }
A2: { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } is empty
proof
assume not { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } is empty ; :: thesis: contradiction
then consider x being object such that
A3: x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } ;
consider f being Function of (Segm (n + 1)),(Segm (k + 1)) such that
x = f and
( f is onto & f is "increasing ) and
A4: f " {(f . n)} = {n} by A3;
0 in Segm (n + 1) by NAT_1:44;
then A5: 0 in dom f by FUNCT_2:def 1;
A6: 0 in by TARSKI:def 1;
A7: f . 0 = 0 by ;
f . n = 0 by ;
then 0 in {n} by ;
hence contradiction by A1; :: thesis: verum
end;
n block k = 0 by ;
hence card { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } by A2; :: thesis: verum
end;
suppose A8: ( k = 0 implies n = 0 ) ; :: thesis: card { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }
defpred S1[ object , set , set ] means for i, j being Nat st Segm i = \$2 & Segm j = \$3 holds
ex f being Function of (Segm i),(Segm j) st
( f = \$1 & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) );
A9: not n in Segm n ;
set FF2 = { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } ;
set FF1 = { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } ;
A10: for f being Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) st f . n = k holds
( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] iff S1[f | (Segm n), Segm n, Segm k] )
proof
let f9 be Function of ((Segm n) \/ {n}),((Segm k) \/ {k}); :: thesis: ( f9 . n = k implies ( S1[f9,(Segm n) \/ {n},(Segm k) \/ {k}] iff S1[f9 | (Segm n), Segm n, Segm k] ) )
assume A11: f9 . n = k ; :: thesis: ( S1[f9,(Segm n) \/ {n},(Segm k) \/ {k}] iff S1[f9 | (Segm n), Segm n, Segm k] )
thus ( S1[f9,(Segm n) \/ {n},(Segm k) \/ {k}] implies S1[f9 | (Segm n), Segm n, Segm k] ) :: thesis: ( S1[f9 | (Segm n), Segm n, Segm k] implies S1[f9,(Segm n) \/ {n},(Segm k) \/ {k}] )
proof
n <= n + 1 by NAT_1:11;
then A12: Segm n c= Segm (n + 1) by NAT_1:39;
A13: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;
A14: Segm (k + 1) = (Segm k) \/ {k} by AFINSQ_1:2;
assume S1[f9,(Segm n) \/ {n},(Segm k) \/ {k}] ; :: thesis: S1[f9 | (Segm n), Segm n, Segm k]
then consider f being Function of (Segm (n + 1)),(Segm (k + 1)) such that
A15: f = f9 and
A16: ( f is onto & f is "increasing ) and
A17: ( n < n + 1 implies f " {(f . n)} = {n} ) by ;
A18: rng (f | n) c= Segm k by ;
A19: dom (f | n) = (dom f) /\ n by RELAT_1:61;
dom f = n + 1 by FUNCT_2:def 1;
then dom (f | n) = n by ;
then reconsider fn = f | n as Function of n,k by ;
let i, j be Nat; :: thesis: ( Segm i = Segm n & Segm j = Segm k implies ex f being Function of (Segm i),(Segm j) st
( f = f9 | (Segm n) & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) )

assume that
A20: Segm i = Segm n and
A21: Segm j = Segm k ; :: thesis: ex f being Function of (Segm i),(Segm j) st
( f = f9 | (Segm n) & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) )

reconsider fi = fn as Function of (Segm i),(Segm j) by ;
( fi is onto & fi is "increasing ) by ;
hence ex f being Function of (Segm i),(Segm j) st
( f = f9 | (Segm n) & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) by ; :: thesis: verum
end;
thus ( S1[f9 | (Segm n), Segm n, Segm k] implies S1[f9,(Segm n) \/ {n},(Segm k) \/ {k}] ) :: thesis: verum
proof
(Segm n) \/ {n} = Segm (n + 1) by AFINSQ_1:2;
then reconsider f = f9 as Function of (Segm (n + 1)),(Segm (k + 1)) by AFINSQ_1:2;
assume S1[f9 | (Segm n), Segm n, Segm k] ; :: thesis: S1[f9,(Segm n) \/ {n},(Segm k) \/ {k}]
then A22: ex fn being Function of (Segm n),(Segm k) st
( fn = f9 | n & fn is onto & fn is "increasing & ( n < n implies fn " {(fn . n)} = {n} ) ) ;
let i, j be Nat; :: thesis: ( Segm i = (Segm n) \/ {n} & Segm j = (Segm k) \/ {k} implies ex f being Function of (Segm i),(Segm j) st
( f = f9 & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) )

assume that
A23: Segm i = (Segm n) \/ {n} and
A24: Segm j = (Segm k) \/ {k} ; :: thesis: ex f being Function of (Segm i),(Segm j) st
( f = f9 & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) )

reconsider f1 = f as Function of (Segm i),(Segm j) by ;
A25: for f being Function of (Segm n),(Segm k)
for f1 being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f = f1 | (Segm n) & f1 . n = k holds
f1 " {(f1 . n)} = {n} by Th40;
A26: ( n < i implies f1 " {(f1 . n)} = {n} ) by ;
A27: Segm (k + 1) = j by ;
Segm (n + 1) = i by ;
then ( f1 is onto & f1 is "increasing ) by ;
hence ex f being Function of (Segm i),(Segm j) st
( f = f9 & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) by A26; :: thesis: verum
end;
end;
A28: ( Segm k is empty implies Segm n is empty ) by A8;
A29: card { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } = card { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } from A30: { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } c= { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } or x in { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } )
assume x in { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } ; :: thesis: x in { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] }
then A31: ex f being Function of (Segm n),(Segm k) st
( x = f & f is onto & f is "increasing ) ;
then S1[x,n,k] ;
hence
x in { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } by A31; :: thesis: verum
end;
A32: { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } c= { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } or x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } )
assume x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } ; :: thesis: x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) }
then consider f being Function of (Segm (n + 1)),(Segm (k + 1)) such that
A33: f = x and
A34: ( f is onto & f is "increasing ) and
A35: f " {(f . n)} = {n} ;
A36: rng (f | n) c= Segm k by ;
A37: S1[f,(Segm n) \/ {n},(Segm k) \/ {k}]
proof
let i, j be Nat; :: thesis: ( Segm i = (Segm n) \/ {n} & Segm j = (Segm k) \/ {k} implies ex f being Function of (Segm i),(Segm j) st
( f = f & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) )

assume that
A38: Segm i = (Segm n) \/ {n} and
A39: Segm j = (Segm k) \/ {k} ; :: thesis: ex f being Function of (Segm i),(Segm j) st
( f = f & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) )

A40: Segm j = Segm (k + 1) by ;
Segm i = Segm (n + 1) by ;
hence ex f being Function of (Segm i),(Segm j) st
( f = f & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) by ; :: thesis: verum
end;
A41: Segm (k + 1) = (Segm k) \/ {k} by AFINSQ_1:2;
A42: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;
f . n = k by ;
hence x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } by A33, A37, A36, A42, A41; :: thesis: verum
end;
A43: { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } c= { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } or x in { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } )
assume x in { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } ; :: thesis: x in { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }
then consider f being Function of n,k such that
A44: x = f and
A45: S1[f,n,k] ;
ex g being Function of (Segm n),(Segm k) st
( g = f & g is onto & g is "increasing & ( n < n implies g " {(g . n)} = {n} ) ) by A45;
hence x in { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } by A44; :: thesis: verum
end;
{ f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } c= { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } or x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } )
assume x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } ; :: thesis: x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) }
then consider f being Function of (n \/ {n}),(k \/ {k}) such that
A46: x = f and
A47: S1[f,n \/ {n},k \/ {k}] and
rng (f | n) c= k and
f . n = k ;
A48: Segm (k + 1) = (Segm k) \/ {k} by AFINSQ_1:2;
Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;
then ex f9 being Function of (Segm (n + 1)),(Segm (k + 1)) st
( f = f9 & f9 is onto & f9 is "increasing & ( n < n + 1 implies f9 " {(f9 . n)} = {n} ) ) by ;
hence x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } by ; :: thesis: verum
end;
then { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } by A32;
hence card { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } by ; :: thesis: verum
end;
end;
end;
hence card { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } ; :: thesis: verum