let k, n be Nat; :: thesis:
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 ) } ;

suppose A1: ( k = 0 & n <> 0 ) ; :: thesis:

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:
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 {0} by TARSKI:def 1;
A7: f . 0 = 0 by A1, CARD_1:49, TARSKI:def 1;
f . n = 0 by A1, CARD_1:49, TARSKI:def 1;
then 0 in {n} by A4, A7, A5, A6, FUNCT_1:def 7;
hence contradiction by A1; :: thesis:

end;

n block k = 0 by A1, Th31;
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:

end;

suppose A8: ( k = 0 implies n = 0 ) ; :: thesis:

defpred S₁[ 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) : S₁[f, Segm n, Segm k] } ;
set FF1 = { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S₁[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
( S₁[f,(Segm n) \/ {n},(Segm k) \/ {k}] iff S₁[f | (Segm n), Segm n, Segm k] )

proof

let f9 be Function of ((Segm n) \/ {n}),((Segm k) \/ {k}); :: thesis:
assume A11: f9 . n = k ; :: thesis:
thus ( S₁[f9,(Segm n) \/ {n},(Segm k) \/ {k}] implies S₁[f9 | (Segm n), Segm n, Segm k] ) :: thesis:

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 S₁[f9,(Segm n) \/ {n},(Segm k) \/ {k}] ; :: thesis:
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 A13, A14;
A18: rng (f | n) c= Segm k by A16, A17, Th37, NAT_1:13;
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 A12, A19, XBOOLE_1:28;
then reconsider fn = f | n as Function of n,k by A18, FUNCT_2:2;
let i, j be Nat; :: thesis:
assume that
A20: Segm i = Segm n and
A21: Segm j = Segm k ; :: thesis:
reconsider fi = fn as Function of (Segm i),(Segm j) by A20, A21;
( fi is onto & fi is "increasing ) by A16, A17, A20, A21, Th37, NAT_1:13;
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 A15, A20; :: thesis:

end;

thus ( S₁[f9 | (Segm n), Segm n, Segm k] implies S₁[f9,(Segm n) \/ {n},(Segm k) \/ {k}] ) :: thesis:

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 S₁[f9 | (Segm n), Segm n, Segm k] ; :: thesis:
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:
assume that
A23: Segm i = (Segm n) \/ {n} and
A24: Segm j = (Segm k) \/ {k} ; :: thesis:
reconsider f1 = f as Function of (Segm i),(Segm j) by A23, A24;
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 A11, A22, A25;
A27: Segm (k + 1) = j by A24, AFINSQ_1:2;
Segm (n + 1) = i by A23, AFINSQ_1:2;
then ( f1 is onto & f1 is "increasing ) by A11, A22, A27, Th40;
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:

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) : S₁[f, Segm n, Segm k] } = card { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S₁[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } from STIRL2_1:sch 4(A28, A9, A10);
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) : S₁[f, Segm n, Segm k] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } ; :: thesis:
then A31: ex f being Function of (Segm n),(Segm k) st
( x = f & f is onto & f is "increasing ) ;
then S₁[x,n,k] ;
hence x in { f where f is Function of (Segm n),(Segm k) : S₁[f, Segm n, Segm k] } by A31; :: thesis:

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}) : ( S₁[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:
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:
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 A34, A35, Th37;
A37: S₁[f,(Segm n) \/ {n},(Segm k) \/ {k}]

proof

let i, j be Nat; :: thesis:
assume that
A38: Segm i = (Segm n) \/ {n} and
A39: Segm j = (Segm k) \/ {k} ; :: thesis:
A40: Segm j = Segm (k + 1) by A39, AFINSQ_1:2;
Segm i = Segm (n + 1) by A38, AFINSQ_1:2;
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 A34, A35, A40; :: thesis:

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 A34, A35, Th34;
hence x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S₁[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } by A33, A37, A36, A42, A41; :: thesis:

end;

A43: { f where f is Function of (Segm n),(Segm k) : S₁[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:
assume x in { f where f is Function of (Segm n),(Segm k) : S₁[f, Segm n, Segm k] } ; :: thesis:
then consider f being Function of n,k such that
A44: x = f and
A45: S₁[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:

end;

{ f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S₁[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:
assume x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S₁[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) } ; :: thesis:
then consider f being Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) such that
A46: x = f and
A47: S₁[f,(Segm n) \/ {n},(Segm k) \/ {k}] and
rng (f | (Segm n)) c= Segm 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 A47, A48;
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 A46, NAT_1:13; :: thesis:

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}) : ( S₁[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 A29, A30, A43, XBOOLE_0:def 10; :: thesis:

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: