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 A1, Th31;
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 S₁[ 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) : S₁[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) : ( S₁[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 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) : ( S₁[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) : ( S₁[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) : ( S₁[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) : ( S₁[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 & S₁[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) : ( S₁[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) : ( S₁[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) : ( S₁[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) : ( S₁[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) : ( S₁[g] & g . n = fi ) } by A16;
then card { g where g is Function of (Segm (n + 1)),(Segm k) : ( S₁[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; :: 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) : S₁[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) : S₁[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) : S₁[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) : S₁[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) : S₁[g] } ; :: thesis: verum

end;

A19: { g where g is Function of (Segm (n + 1)),(Segm k) : S₁[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) : S₁[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) : S₁[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 & S₁[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 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; :: 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