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

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 ) } 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: verumper cases
not ( not ( k = 0 & n <> 0 ) & k = 0 & not n = 0 )
;

end;

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

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;proof

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

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

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

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 S_{1}[ 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_{1}[f, Segm n, Segm k] } ;

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

A29: card { f where f is Function of (Segm n),(Segm k) : S_{1}[f, Segm n, Segm k] } = card { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S_{1}[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_{1}[f, Segm n, Segm k] }
_{1}[f,(Segm n) \/ {n},(Segm k) \/ {k}] & rng (f | (Segm n)) c= Segm k & f . n = k ) }
_{1}[f, Segm n, Segm k] } c= { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }
_{1}[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} ) }
_{1}[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: verum

end;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

set FF1 = { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S

A10: for f being Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) st f . n = k holds

( S

proof

A28:
( Segm k is empty implies Segm n is empty )
by A8;
let f9 be Function of ((Segm n) \/ {n}),((Segm k) \/ {k}); :: thesis: ( f9 . n = k implies ( S_{1}[f9,(Segm n) \/ {n},(Segm k) \/ {k}] iff S_{1}[f9 | (Segm n), Segm n, Segm k] ) )

assume A11: f9 . n = k ; :: thesis: ( S_{1}[f9,(Segm n) \/ {n},(Segm k) \/ {k}] iff S_{1}[f9 | (Segm n), Segm n, Segm k] )

thus ( S_{1}[f9,(Segm n) \/ {n},(Segm k) \/ {k}] implies S_{1}[f9 | (Segm n), Segm n, Segm k] )
:: thesis: ( S_{1}[f9 | (Segm n), Segm n, Segm k] implies S_{1}[f9,(Segm n) \/ {n},(Segm k) \/ {k}] )_{1}[f9 | (Segm n), Segm n, Segm k] implies S_{1}[f9,(Segm n) \/ {n},(Segm k) \/ {k}] )
:: thesis: verum

end;assume A11: f9 . n = k ; :: thesis: ( S

thus ( S

proof

thus
( S
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_{1}[f9,(Segm n) \/ {n},(Segm k) \/ {k}]
; :: thesis: S_{1}[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 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: ( 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 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: verum

end;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

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: ( 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 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: 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 S_{1}[f9 | (Segm n), Segm n, Segm k]
; :: thesis: S_{1}[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 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: verum

end;then reconsider f = f9 as Function of (Segm (n + 1)),(Segm (k + 1)) by AFINSQ_1:2;

assume S

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

A29: card { f where f is Function of (Segm n),(Segm k) : S

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

proof

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
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) : S_{1}[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) : S_{1}[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 S_{1}[x,n,k]
;

hence x in { f where f is Function of (Segm n),(Segm k) : S_{1}[f, Segm n, Segm k] }
by A31; :: thesis: verum

end;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) : S

then A31: ex f being Function of (Segm n),(Segm k) st

( x = f & f is onto & f is "increasing ) ;

then S

hence x in { f where f is Function of (Segm n),(Segm k) : S

proof

A43:
{ f where f is Function of (Segm n),(Segm k) : S
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}) : ( S_{1}[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}) : ( S_{1}[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 A34, A35, Th37;

A37: S_{1}[f,(Segm n) \/ {n},(Segm k) \/ {k}]

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_{1}[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;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}) : ( S

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

proof

A41:
Segm (k + 1) = (Segm k) \/ {k}
by AFINSQ_1:2;
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 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: verum

end;( 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 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: verum

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

proof

{ f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm n),(Segm k) : S_{1}[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) : S_{1}[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: S_{1}[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;assume x in { f where f is Function of (Segm n),(Segm k) : S

then consider f being Function of n,k such that

A44: x = f and

A45: S

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

proof

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
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}) : ( S_{1}[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}) : ( S_{1}[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: S_{1}[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 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: verum

end;assume x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {k}) : ( S

then consider f being Function of (n \/ {n}),(k \/ {k}) such that

A46: x = f and

A47: S

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

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