let k, n be Nat; k * (n block k) = card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }
now k * (n block k) = card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } per cases
( k = 0 or k > 0 )
;
suppose
k > 0
;
k * (n block k) = card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } then A3:
not
Segm k is
empty
;
set G1 =
{ g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } ;
defpred S1[
set ]
means ex
f being
Function of
(Segm (n + 1)),
(Segm k) st
(
f = $1 &
f is
onto &
f is
"increasing &
f " {(f . n)} <> {n} );
n < n + 1
by NAT_1:13;
then A4:
n in Segm (n + 1)
by NAT_1:44;
consider f being
Function such that A5:
f is
one-to-one
and A6:
dom f = card k
and A7:
rng f = k
by WELLORD2:def 4;
reconsider f =
f as
Function of
(card (Segm k)),
(Segm k) by A6, A7, FUNCT_2:1;
A8:
(
f is
onto &
f is
one-to-one )
by A5, A7, FUNCT_2:def 3;
consider F being
XFinSequence of
NAT such that A9:
dom F = card (Segm k)
and A10:
card { g where g is Function of (Segm (n + 1)),(Segm k) : S1[g] } = Sum F
and A11:
for
i being
Nat st
i in dom F holds
F . i = card { g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = f . i ) }
from STIRL2_1:sch 6(A8, A3, A4);
A12:
for
i being
Nat st
i in dom F holds
F . i = n block k
proof
set F2 =
{ g where g is Function of (Segm n),(Segm k) : ( g is onto & g is "increasing ) } ;
let i be
Nat;
( i in dom F implies F . i = n block k )
assume A13:
i in dom F
;
F . i = n block k
A14:
f . i in rng f
by A6, A9, A13, FUNCT_1:def 3;
reconsider fi =
f . i as
Element of
NAT by A7, A14;
A15:
fi < k
by A14, NAT_1:44;
set F1 =
{ g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) } ;
set F =
{ g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } ;
A16:
{ g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) } c= { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) }
{ g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } c= { g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) }
then
{ g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } = { g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) }
by A16;
then
card { g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) } = card { g where g is Function of (Segm n),(Segm k) : ( g is onto & g is "increasing ) }
by A15, Th43;
hence
F . i = n block k
by A11, A13;
verum
end; then
for
i being
Nat st
i in dom F holds
F . i <= n block k
;
then A17:
Sum F <= (len F) * (n block k)
by AFINSQ_2:59;
set G =
{ g where g is Function of (Segm (n + 1)),(Segm k) : S1[g] } ;
A18:
{ g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } c= { g where g is Function of (Segm (n + 1)),(Segm k) : S1[g] }
A19:
{ g where g is Function of (Segm (n + 1)),(Segm k) : S1[g] } c= { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) }
for
i being
Nat st
i in dom F holds
F . i >= n block k
by A12;
then A20:
Sum F >= (len F) * (n block k)
by AFINSQ_2:60;
Sum F = k * (n block k)
by A9, A17, A20, XXREAL_0:1;
hence
k * (n block k) = card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }
by A10, A18, A19, XBOOLE_0:def 10;
verum end; end; end;
hence
k * (n block k) = card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }
; verum