let k, n be Nat; :: thesis: 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 :: thesis: 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 A1: k = 0 ; :: thesis: 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} ) }
reconsider F1 = { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing ) } as set ;
reconsider F = { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } as set ;
A2: F c= F1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in F1 )
assume x in F ; :: thesis: x in F1
then ex f being Function of (Segm (n + 1)),(Segm k) st
( x = f & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ;
hence x in F1 ; :: thesis: verum
end;
card F1 = (n + 1) block k ;
then F1 is empty by ;
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 A1, A2; :: thesis: verum
end;
suppose k > 0 ; :: thesis: 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 ;
A8: ( f is onto & f is one-to-one ) by ;
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; :: 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 by ;
reconsider fi = f . i as Element of NAT by ;
A15: fi < k by ;
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 ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) } or x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } )
assume x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) } ; :: thesis: x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) }
then ex g being Function of (Segm (n + 1)),(Segm k) st
( x = g & S1[g] & g . n = fi ) ;
hence x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } ; :: thesis: verum
end;
{ 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 ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } or x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) } )
assume x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } ; :: thesis: x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) }
then ex g being Function of (Segm (n + 1)),(Segm k) st
( x = g & g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) ;
hence x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( S1[g] & g . n = fi ) } ; :: thesis: verum
end;
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 ;
hence F . i = n block k by ; :: thesis: 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] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } or x in { g where g is Function of (Segm (n + 1)),(Segm k) : S1[g] } )
assume x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } ; :: thesis: x in { g where g is Function of (Segm (n + 1)),(Segm k) : S1[g] }
then ex g being Function of (Segm (n + 1)),(Segm k) st
( x = g & g is onto & g is "increasing & g " {(g . n)} <> {n} ) ;
hence x in { g where g is Function of (Segm (n + 1)),(Segm k) : S1[g] } ; :: thesis: verum
end;
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} ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of (Segm (n + 1)),(Segm k) : S1[g] } or x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } )
assume x in { g where g is Function of (Segm (n + 1)),(Segm k) : S1[g] } ; :: thesis: x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) }
then ex g being Function of (Segm (n + 1)),(Segm k) st
( x = g & S1[g] ) ;
hence x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } ; :: thesis: verum
end;
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 ;
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 ; :: thesis: 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} ) } ; :: thesis: verum