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

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

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) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } ;

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

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) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } ;

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

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

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

A3: 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) \/ {l}) : ( S_{1}[f,(Segm n) \/ {n},(Segm k) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) } ;

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

( S_{1}[f,(Segm n) \/ {n},(Segm k) \/ {l}] iff S_{1}[f | (Segm n), Segm n, Segm k] )

A22: 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) \/ {l}) : ( S_{1}[f,(Segm n) \/ {n},(Segm k) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) }
from STIRL2_1:sch 4(A21, A3, A4);

A23: { 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) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) }
_{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) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) } c= { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) }
_{1}[f,(Segm n) \/ {n},(Segm k) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) }
by A25;

hence card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } by A22, A23, A36, 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} ) );

A3: 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) \/ {l}) : ( S

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

( S

proof

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

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

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

end;assume A5: f9 . n = l ; :: thesis: ( S

thus ( S

proof

thus
( S
n <= n + 1
by NAT_1:13;

then A6: Segm n c= Segm (n + 1) by NAT_1:39;

assume A7: S_{1}[f9,(Segm n) \/ {n},(Segm k) \/ {l}]
; :: thesis: S_{1}[f9 | (Segm n), Segm n, Segm k]

A8: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

k = k \/ {l} by A1, Lm1;

then consider f being Function of (Segm (n + 1)),(Segm 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;

rng (f | n) c= rng f by RELAT_1:70;

then A13: rng (f | n) c= Segm k by XBOOLE_1:1;

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 (Segm n),(Segm k) by A13, 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

A14: Segm i = Segm n and

A15: 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 A14, A15;

( fi is onto & fi is "increasing ) by A10, A11, A14, A15, Th38, 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 A9, A14; :: thesis: verum

end;then A6: Segm n c= Segm (n + 1) by NAT_1:39;

assume A7: S

A8: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

k = k \/ {l} by A1, Lm1;

then consider f being Function of (Segm (n + 1)),(Segm 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;

rng (f | n) c= rng f by RELAT_1:70;

then A13: rng (f | n) c= Segm k by XBOOLE_1:1;

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 (Segm n),(Segm k) by A13, 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

A14: Segm i = Segm n and

A15: 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 A14, A15;

( fi is onto & fi is "increasing ) by A10, A11, A14, A15, Th38, 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 A9, A14; :: thesis: verum

proof

(Segm n) \/ {n} = Segm (n + 1)
by AFINSQ_1:2;

then reconsider f = f9 as Function of (n + 1),k by A1, Lm1;

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

then A16: 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) \/ {l} 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

A17: Segm i = (Segm n) \/ {n} and

A18: Segm j = (Segm k) \/ {l} ; :: 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 A17, A18;

for f being Function of (Segm n),(Segm k)

for g being Function of (Segm (n + 1)),(Segm k) st f is onto & f is "increasing & f = g | (Segm n) & g . n < k holds

( g is onto & g is "increasing & g " {(g . n)} <> {n} ) by Th41;

then A19: ( n < i implies f1 " {(f1 . n)} <> {n} ) by A1, A5, A16;

A20: Segm (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 (Segm i),(Segm j) st

( f = f9 & f is onto & f is "increasing & ( n < i implies f " {(f . n)} <> {n} ) ) by A19; :: thesis: verum

end;then reconsider f = f9 as Function of (n + 1),k by A1, Lm1;

assume S

then A16: 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) \/ {l} 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

A17: Segm i = (Segm n) \/ {n} and

A18: Segm j = (Segm k) \/ {l} ; :: 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 A17, A18;

for f being Function of (Segm n),(Segm k)

for g being Function of (Segm (n + 1)),(Segm k) st f is onto & f is "increasing & f = g | (Segm n) & g . n < k holds

( g is onto & g is "increasing & g " {(g . n)} <> {n} ) by Th41;

then A19: ( n < i implies f1 " {(f1 . n)} <> {n} ) by A1, A5, A16;

A20: Segm (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 (Segm i),(Segm j) st

( f = f9 & f is onto & f is "increasing & ( n < i implies f " {(f . n)} <> {n} ) ) by A19; :: thesis: verum

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

A23: { 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

A25:
{ f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } c= { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( 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 A24: 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 A24; :: 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 A24: 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

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

assume x in { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } ; :: thesis: x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S_{1}[f,(Segm n) \/ {n},(Segm k) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) }

then consider f being Function of (Segm (n + 1)),(Segm 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_{1}[f,(Segm n) \/ {n},(Segm k) \/ {l}]

A35: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

rng (f | (Segm n)) c= rng f by RELAT_1:70;

then rng (f | (Segm n)) c= Segm k by XBOOLE_1:1;

hence x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S_{1}[f,(Segm n) \/ {n},(Segm k) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) }
by A26, A29, A30, A35, A34; :: thesis: verum

end;assume x in { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } ; :: thesis: x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S

then consider f being Function of (Segm (n + 1)),(Segm 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

proof

A34:
k = k \/ {l}
by A1, Lm1;
let i, j be Nat; :: thesis: ( Segm i = (Segm n) \/ {n} & Segm j = (Segm k) \/ {l} 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

A31: Segm i = (Segm n) \/ {n} and

A32: Segm j = (Segm k) \/ {l} ; :: 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} ) )

A33: i = Segm (n + 1) by A31, AFINSQ_1:2;

j = k by A1, A32, Lm1;

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 A27, A28, A33; :: thesis: verum

end;( f = f & f is onto & f is "increasing & ( n < i implies f " {(f . n)} <> {n} ) ) )

assume that

A31: Segm i = (Segm n) \/ {n} and

A32: Segm j = (Segm k) \/ {l} ; :: 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} ) )

A33: i = Segm (n + 1) by A31, AFINSQ_1:2;

j = k by A1, A32, Lm1;

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 A27, A28, A33; :: thesis: verum

A35: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

rng (f | (Segm n)) c= rng f by RELAT_1:70;

then rng (f | (Segm n)) c= Segm k by XBOOLE_1:1;

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

proof

{ f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( 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

A37: x = f and

A38: 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 A38;

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

A37: x = f and

A38: 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 A38;

hence x in { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } by A37; :: thesis: verum

proof

then
{ f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S
A39:
Segm (n + 1) = (Segm n) \/ {n}
by AFINSQ_1:2;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S_{1}[f,(Segm n) \/ {n},(Segm k) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) } or x in { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } )

assume x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S_{1}[f,(Segm n) \/ {n},(Segm k) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) }
; :: thesis: x in { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) }

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

A40: x = f and

A41: S_{1}[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 (Segm (n + 1)),(Segm 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 (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } by A40, A42, NAT_1:13; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S

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

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

A40: x = f and

A41: S

rng (f | n) c= k and

A42: f . n = l ;

k = k \/ {l} by A1, Lm1;

then ex f9 being Function of (Segm (n + 1)),(Segm 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 (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } by A40, A42, NAT_1:13; :: thesis: verum

hence card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } by A22, A23, A36, XBOOLE_0:def 10; :: thesis: verum