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