let n, k be Nat; :: thesis:
set F1 = { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } ;
set F2 = { f where f is Function of n,k : ( f is onto & f is "increasing ) } ;

A2: { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } is empty

assume not { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } is empty ; :: thesis:
then consider x being set such that
A3: x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } by XBOOLE_0:def 1;
consider f being Function of (n + 1),(k + 1) such that
x = f and
( f is onto & f is "increasing ) and
A4: f " {(f . n)} = {n} by A3;
0 in 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, TARSKI:def 1; :: thesis:

end;

n block k = 0 by A1, Th31;
hence card { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) } by A2; :: thesis:

end;

defpred S₁[ set , set , set ] means for i, j being Nat st i = $2 & j = $3 holds
ex f being Function of i,j st
( f = $1 & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) );
A9: not n in n ;
set FF2 = { f where f is Function of n,k : S₁[f,n,k] } ;
set FF1 = { f where f is Function of (n \/ {n}),(k \/ {k}) : ( S₁[f,n \/ {n},k \/ {k}] & rng (f | n) c= k & f . n = k ) } ;
A10: for f being Function of (n \/ {n}),(k \/ {k}) st f . n = k holds
( S₁[f,n \/ {n},k \/ {k}] iff S₁[f | n,n,k] )

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

n <= n + 1 by NAT_1:11;
then A12: n c= n + 1 by NAT_1:39;
A13: n + 1 = n \/ {n} by AFINSQ_1:2;
A14: k + 1 = k \/ {k} by AFINSQ_1:2;
assume S₁[f9,n \/ {n},k \/ {k}] ; :: thesis:
then consider f being Function of (n + 1),(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= 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: i = n and
A21: j = k ; :: thesis:
reconsider fi = fn as Function of i,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 i,j st
( f = f9 | n & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) by A15, A20; :: thesis:

end;

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

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

end;

A27: ( k is empty implies n is empty ) by A8;
A28: card { f where f is Function of n,k : S₁[f,n,k] } = card { f where f is Function of (n \/ {n}),(k \/ {k}) : ( S₁[f,n \/ {n},k \/ {k}] & rng (f | n) c= k & f . n = k ) } from STIRL2_1:sch 4(A27, A9, A10);
A29: { f where f is Function of n,k : ( f is onto & f is "increasing ) } c= { f where f is Function of n,k : S₁[f,n,k] }

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

end;

A31: { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } c= { f where f is Function of (n \/ {n}),(k \/ {k}) : ( S₁[f,n \/ {n},k \/ {k}] & rng (f | n) c= k & f . n = k ) }

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } ; :: thesis:
then consider f being Function of (n + 1),(k + 1) such that
A32: f = x and
A33: ( f is onto & f is "increasing ) and
A34: f " {(f . n)} = {n} ;
A35: rng (f | n) c= k by A33, A34, Th37;
A36: S₁[f,n \/ {n},k \/ {k}]

let i, j be Nat; :: thesis:
assume that
A37: i = n \/ {n} and
A38: j = k \/ {k} ; :: thesis:
A39: j = k + 1 by A38, AFINSQ_1:2;
i = n + 1 by A37, AFINSQ_1:2;
hence ex f being Function of i,j st
( f = f & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) by A33, A34, A39; :: thesis:

end;

A40: k + 1 = k \/ {k} by AFINSQ_1:2;
A41: n + 1 = n \/ {n} by AFINSQ_1:2;
f . n = k by A33, A34, Th34;
hence x in { f where f is Function of (n \/ {n}),(k \/ {k}) : ( S₁[f,n \/ {n},k \/ {k}] & rng (f | n) c= k & f . n = k ) } by A32, A36, A35, A41, A40; :: thesis:

end;

A42: { f where f is Function of n,k : S₁[f,n,k] } c= { f where f is Function of n,k : ( f is onto & f is "increasing ) }

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { f where f is Function of n,k : S₁[f,n,k] } ; :: thesis:
then consider f being Function of n,k such that
A43: x = f and
A44: S₁[f,n,k] ;
ex g being Function of n,k st
( g = f & g is onto & g is "increasing & ( n < n implies g " {(g . n)} = {n} ) ) by A44;
hence x in { f where f is Function of n,k : ( f is onto & f is "increasing ) } by A43; :: thesis:

end;

{ f where f is Function of (n \/ {n}),(k \/ {k}) : ( S₁[f,n \/ {n},k \/ {k}] & rng (f | n) c= k & f . n = k ) } c= { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) }

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { f where f is Function of (n \/ {n}),(k \/ {k}) : ( S₁[f,n \/ {n},k \/ {k}] & rng (f | n) c= k & f . n = k ) } ; :: thesis:
then consider f being Function of (n \/ {n}),(k \/ {k}) such that
A45: x = f and
A46: S₁[f,n \/ {n},k \/ {k}] and
rng (f | n) c= k and
f . n = k ;
A47: k + 1 = k \/ {k} by AFINSQ_1:2;
n + 1 = n \/ {n} by AFINSQ_1:2;
then ex f9 being Function of (n + 1),(k + 1) st
( f = f9 & f9 is onto & f9 is "increasing & ( n < n + 1 implies f9 " {(f9 . n)} = {n} ) ) by A46, A47;
hence x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } by A45, NAT_1:13; :: thesis:

end;

then { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = { f where f is Function of (n \/ {n}),(k \/ {k}) : ( S₁[f,n \/ {n},k \/ {k}] & rng (f | n) c= k & f . n = k ) } by A31, XBOOLE_0:def 10;
hence card { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) } by A28, A29, A42, XBOOLE_0:def 10; :: thesis:

end;

hence card { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) } ; :: thesis: