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 ) } ;
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 ) }
per cases not ( not ( k = 0 & n <> 0 ) & k = 0 & not n = 0 ) ;
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 S1[ 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) : S1[f, Segm n, Segm k] } ;
set FF1 = { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S1[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
( S1[f,(Segm n) \/ {n},(Segm k) \/ {l}] iff S1[f | (Segm n), Segm n, Segm k] )
proof
let f9 be Function of ((Segm n) \/ {n}),((Segm k) \/ {l}); :: thesis: ( f9 . n = l implies ( S1[f9,(Segm n) \/ {n},(Segm k) \/ {l}] iff S1[f9 | (Segm n), Segm n, Segm k] ) )
assume A5: f9 . n = l ; :: thesis: ( S1[f9,(Segm n) \/ {n},(Segm k) \/ {l}] iff S1[f9 | (Segm n), Segm n, Segm k] )
thus ( S1[f9,(Segm n) \/ {n},(Segm k) \/ {l}] implies S1[f9 | (Segm n), Segm n, Segm k] ) :: thesis: ( S1[f9 | (Segm n), Segm n, Segm k] implies S1[f9,(Segm n) \/ {n},(Segm k) \/ {l}] )
proof
n <= n + 1 by NAT_1:13;
then A6: Segm n c= Segm (n + 1) by NAT_1:39;
assume A7: S1[f9,(Segm n) \/ {n},(Segm k) \/ {l}] ; :: thesis: S1[f9 | (Segm n), Segm n, Segm k]
A8: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;
k = k \/ {l} by ;
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 ;
then dom (f | n) = n by ;
then reconsider fn = f | n as Function of (Segm n),(Segm k) by ;
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 ;
( fi is onto & fi is "increasing ) by ;
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 ; :: thesis: verum
end;
thus ( S1[f9 | (Segm n), Segm n, Segm k] implies S1[f9,(Segm n) \/ {n},(Segm k) \/ {l}] ) :: thesis: verum
proof
(Segm n) \/ {n} = Segm (n + 1) by AFINSQ_1:2;
then reconsider f = f9 as Function of (n + 1),k by ;
assume S1[f9 | (Segm n), Segm n, Segm k] ; :: thesis: S1[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 ;
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 ;
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;
end;
A21: ( Segm k is empty implies Segm n is empty ) by A2;
A22: card { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } = card { f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) } from 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) : S1[f, Segm n, Segm k] }
proof
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) : S1[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) : S1[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 S1[x,n,k] ;
hence
x in { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } by A24; :: thesis: verum
end;
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}) : ( S1[f,(Segm n) \/ {n},(Segm k) \/ {l}] & rng (f | (Segm n)) c= Segm k & f . n = l ) }
proof
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}) : ( S1[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}) : ( S1[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: S1[f,(Segm n) \/ {n},(Segm k) \/ {l}]
proof
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 ;
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 ; :: thesis: verum
end;
A34: k = k \/ {l} by ;
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}) : ( S1[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;
A36: { f where f is Function of (Segm n),(Segm k) : S1[f, Segm n, Segm k] } c= { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm n),(Segm k) : S1[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) : S1[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: S1[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;
{ f where f is Function of ((Segm n) \/ {n}),((Segm k) \/ {l}) : ( S1[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 ) }
proof
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}) : ( S1[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}) : ( S1[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: S1[f,n \/ {n},k \/ {l}] and
rng (f | n) c= k and
A42: f . n = l ;
k = k \/ {l} by ;
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 ;
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 ; :: thesis: verum
end;
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}) : ( S1[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 ; :: thesis: verum
end;
end;
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: verum