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

now

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 (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 ) }

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

proof

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: contradiction
then consider x being set such that
A2: 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
A3: ( x = f & f is onto & f is "increasing & f " {(f . n)} = {n} ) by A2;
( 0 < n + 1 & n < n + 1 ) by NAT_1:13;
then ( k + 1 = {0 } & 0 in n + 1 & n in n + 1 & dom f = n + 1 ) by A1, CARD_1:87, FUNCT_2:def 1, NAT_1:45;
then ( f . n = 0 & f . 0 = 0 & 0 in dom f & 0 in {0 } ) by TARSKI:def 1;
then 0 in {n} by A3, FUNCT_1:def 13;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

then ( card { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } = 0 & 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 ) } ; :: thesis: verum

end;

suppose ( k = 0 implies n = 0 ) ; :: thesis: 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 ) }

then A4: ( k is empty implies n is empty ) ;
defpred S₁[ set , set , set ] means for i, j being Element of 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} ) );
A5: not n in n ;
A6: 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] )

proof

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

proof

assume A8: S₁[f',n \/ {n},k \/ {k}] ; :: thesis: S₁[f' | n,n,k]
( n + 1 = n \/ {n} & k + 1 = k \/ {k} ) by AFINSQ_1:4;
then consider f being Function of (n + 1),(k + 1) such that
A9: ( f = f' & f is onto & f is "increasing & ( n < n + 1 implies f " {(f . n)} = {n} ) ) by A8;
let i, j be Element of NAT ; :: thesis: ( i = n & j = k implies ex f being Function of i,j st
( f = f' | n & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) )
assume A10: ( i = n & j = k ) ; :: thesis: ex f being Function of i,j st
( f = f' | n & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) )
n <= n + 1 by NAT_1:11;
then ( dom f = n + 1 & n c= n + 1 & dom (f | n) = (dom f) /\ n ) by FUNCT_2:def 1, NAT_1:40, RELAT_1:90;
then ( dom (f | n) = n & rng (f | n) c= k ) by A9, Th37, NAT_1:13, XBOOLE_1:28;
then reconsider fn = f | n as Function of n,k by FUNCT_2:4;
reconsider fi = fn as Function of i,j by A10;
( fi = f' | n & fi is onto & fi is "increasing & ( n < i implies fi " {(fi . n)} = {n} ) ) by A9, A10, Th37, NAT_1:13;
hence ex f being Function of i,j st
( f = f' | n & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) ; :: thesis: verum

end;

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

proof

assume S₁[f' | n,n,k] ; :: thesis: S₁[f',n \/ {n},k \/ {k}]
then consider fn being Function of n,k such that
A11: fn = f' | n and
A12: ( fn is onto & fn is "increasing ) and
( n < n implies fn " {(fn . n)} = {n} ) ;
let i, j be Element of NAT ; :: thesis: ( i = n \/ {n} & j = k \/ {k} implies ex f being Function of i,j st
( f = f' & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) )
assume A13: ( i = n \/ {n} & j = k \/ {k} ) ; :: thesis: ex f being Function of i,j st
( f = f' & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) )
( n \/ {n} = n + 1 & k \/ {k} = k + 1 ) by AFINSQ_1:4;
then reconsider f = f' as Function of (n + 1),(k + 1) ;
reconsider f1 = f as Function of i,j by A13;
( n + 1 = i & k + 1 = j ) by A13, AFINSQ_1:4;
then ( f1 is onto & f1 is "increasing & ( n < i implies f1 " {(f1 . n)} = {n} ) ) by A7, A11, A12, Th40;
hence ex f being Function of i,j st
( f = f' & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) ; :: thesis: verum

end;

end;

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 ) } ;
set FF2 = { f where f is Function of n,k : S₁[f,n,k] } ;
A14: 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(A4, A5, A6);
A15: { 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 ) }

proof

thus { 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 ) } :: according to XBOOLE_0:def 10 :: thesis: { 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} ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } or 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 ) } )
assume A16: x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } ; :: thesis: 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 ) }
consider f being Function of (n + 1),(k + 1) such that
A17: ( f = x & f is onto & f is "increasing & f " {(f . n)} = {n} ) by A16;
S₁[f,n \/ {n},k \/ {k}]

proof

let i, j be Element of NAT ; :: thesis: ( i = n \/ {n} & j = k \/ {k} implies ex f being Function of i,j st
( f = f & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) ) )
assume A18: ( i = n \/ {n} & j = k \/ {k} ) ; :: thesis: ex f being Function of i,j st
( f = f & f is onto & f is "increasing & ( n < i implies f " {(f . n)} = {n} ) )
( i = n + 1 & j = k + 1 ) by A18, AFINSQ_1:4;
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 A17; :: thesis: verum

end;

then ( S₁[f,n \/ {n},k \/ {k}] & f . n = k & rng (f | n) c= k & n + 1 = n \/ {n} & k + 1 = k \/ {k} ) by A17, Th34, Th37, AFINSQ_1:4;
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 A17; :: thesis: verum

end;

thus { 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} ) } :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } or x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } )
assume A19: 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: x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) }
consider f being Function of (n \/ {n}),(k \/ {k}) such that
A20: ( x = f & S₁[f,n \/ {n},k \/ {k}] & rng (f | n) c= k & f . n = k ) by A19;
( n + 1 = n \/ {n} & k + 1 = k \/ {k} ) by AFINSQ_1:4;
then ex f' being Function of (n + 1),(k + 1) st
( f = f' & f' is onto & f' is "increasing & ( n < n + 1 implies f' " {(f' . n)} = {n} ) ) by A20;
hence x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } by A20, NAT_1:13; :: thesis: verum

end;

end;

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

proof

thus { 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] } :: according to XBOOLE_0:def 10 :: thesis: { 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 ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of n,k : ( f is onto & f is "increasing ) } or x in { f where f is Function of n,k : S₁[f,n,k] } )
assume A21: x in { f where f is Function of n,k : ( f is onto & f is "increasing ) } ; :: thesis: x in { f where f is Function of n,k : S₁[f,n,k] }
consider f being Function of n,k such that
A22: ( x = f & f is onto & f is "increasing ) by A21;
S₁[x,n,k] by A22;
hence x in { f where f is Function of n,k : S₁[f,n,k] } by A22; :: thesis: verum

end;

thus { 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 ) } :: thesis: verum

proof

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

end;

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 ) } by A14, A15; :: thesis: verum

end;

end;

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: verum