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

hence card { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) } by A1; :: 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 {n} ) );
A3: 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 \/ {l}) : ( S₁[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) } ;
A4: for f being Function of (n \/ {n}),(k \/ {l}) st f . n = l holds
( S₁[f,n \/ {n},k \/ {l}] iff S₁[f | n,n,k] )

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

n <= n + 1 by NAT_1:13;
then A6: n c= n + 1 by NAT_1:39;
assume A7: S₁[f9,n \/ {n},k \/ {l}] ; :: thesis:
A8: n + 1 = n \/ {n} by AFINSQ_1:2;
k = k \/ {l} by A1, Lm1;
then consider f being Function of (n + 1),k such that
A9: f = f9 and
A10: ( f is onto & f is "increasing ) and
A11: ( n < n + 1 implies f " {(f . n)} <> {n} ) by A7, A8;
A12: dom (f | n) = (dom f) /\ n by RELAT_1:61;
A13: rng (f | n) c= k ;
dom f = n + 1 by A1, FUNCT_2:def 1;
then dom (f | n) = n by A6, A12, XBOOLE_1:28;
then reconsider fn = f | n as Function of n,k by A13, FUNCT_2:2;
let i, j be Nat; :: thesis:
assume that
A14: i = n and
A15: j = k ; :: thesis:
reconsider fi = fn as Function of i,j by A14, A15;
( fi is onto & fi is "increasing ) by A10, A11, A14, A15, Th38, NAT_1:13;
hence ex f being Function of i,j st
( f = f9 | n & f is onto & f is "increasing & ( n {n} ) ) by A9, A14; :: thesis:

end;

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

n \/ {n} = n + 1 by AFINSQ_1:2;
then reconsider f = f9 as Function of (n + 1),k by A1, Lm1;
assume S₁[f9 | n,n,k] ; :: thesis:
then A16: 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
A17: i = n \/ {n} and
A18: j = k \/ {l} ; :: thesis:
reconsider f1 = f as Function of i,j by A17, A18;
A19: ( n {n} ) by A1, A5, A16, Th41;
A20: n + 1 = i by A17, AFINSQ_1:2;
k = j by A1, A18, Lm1;
then ( f1 is onto & f1 is "increasing ) by A1, A5, A16, A20, Th41;
hence ex f being Function of i,j st
( f = f9 & f is onto & f is "increasing & ( n {n} ) ) by A19; :: thesis:

end;

A21: ( k is empty implies n is empty ) by A2;
A22: card { f where f is Function of n,k : S₁[f,n,k] } = card { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S₁[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) } from STIRL2_1:sch 4(A21, A3, A4);
A23: { 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 A24: 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 A24; :: thesis:

end;

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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } ; :: thesis:
then consider f being Function of (n + 1),k such that
A26: f = x and
A27: ( f is onto & f is "increasing ) and
A28: f " {(f . n)} <> {n} and
A29: f . n = l ;
A30: S₁[f,n \/ {n},k \/ {l}]

let i, j be Nat; :: thesis:
assume that
A31: i = n \/ {n} and
A32: j = k \/ {l} ; :: thesis:
A33: i = n + 1 by A31, AFINSQ_1:2;
j = k by A1, A32, Lm1;
hence ex f being Function of i,j st
( f = f & f is onto & f is "increasing & ( n {n} ) ) by A27, A28, A33; :: thesis:

end;

A34: k = k \/ {l} by A1, Lm1;
A35: n + 1 = n \/ {n} by AFINSQ_1:2;
rng (f | n) c= k ;
hence x in { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S₁[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) } by A26, A29, A30, A35, A34; :: thesis:

end;

A36: { 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
A37: x = f and
A38: 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 A38;
hence x in { f where f is Function of n,k : ( f is onto & f is "increasing ) } by A37; :: thesis:

end;

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

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

end;

then { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S₁[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) } by A25, XBOOLE_0:def 10;
hence card { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) } by A22, A23, A36, XBOOLE_0:def 10; :: thesis:

end;

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