let k, n, l be Nat; ( 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
; 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 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 A2:
(
k = 0 implies
n = 0 )
;
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});
( 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
;
( 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] )
( 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}]
;
S1[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;
( 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
;
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;
verum
end;
thus
(
S1[
f9 | (Segm n),
Segm n,
Segm k] implies
S1[
f9,
(Segm n) \/ {n},
(Segm k) \/ {l}] )
verumproof
(Segm n) \/ {n} = Segm (n + 1)
by AFINSQ_1:2;
then reconsider f =
f9 as
Function of
(n + 1),
k by A1, Lm1;
assume
S1[
f9 | (Segm n),
Segm n,
Segm k]
;
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;
( 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}
;
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;
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 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) : S1[f, Segm n, Segm k] }
proof
let x be
object ;
TARSKI:def 3 ( 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 ) }
;
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;
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 ;
TARSKI:def 3 ( 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 ) }
;
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}]
A34:
k = k \/ {l}
by A1, Lm1;
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;
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 ;
TARSKI:def 3 ( 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] }
;
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;
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 ;
TARSKI:def 3 ( 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 ) }
;
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
((Segm n) \/ {n}),
((Segm k) \/ {l}) such that A40:
x = f
and A41:
S1[
f,
(Segm n) \/ {n},
(Segm k) \/ {l}]
and
rng (f | (Segm 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;
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 A22, A23, A36, XBOOLE_0:def 10;
verum 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 ) }
; verum