let k, n 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 A1: 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} ) }

set F1 = { f where f is Function of (n + 1),k : ( f is onto & f is "increasing ) } ;
set F = { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ;
A2: { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } c= { f where f is Function of (n + 1),k : ( f is onto & f is "increasing ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } or x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing ) } )
assume x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ; :: thesis: x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing ) }
then ex f being Function of (n + 1),k st
( x = f & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ;
hence x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing ) } ; :: thesis: verum

end;

card { f where f is Function of (n + 1),k : ( f is onto & f is "increasing ) } = (n + 1) block k ;
then { f where f is Function of (n + 1),k : ( f is onto & f is "increasing ) } is empty by A1, Th31;
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 A1, A2; :: thesis: verum

end;

suppose 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} ) }

then A3: not k is empty ;
set G1 = { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } ;
defpred S₁[ set ] means ex f being Function of (n + 1),k st
( f = $1 & f is onto & f is "increasing & f " {(f . n)} <> {n} );
n < n + 1 by NAT_1:13;
then A5: n in n + 1 by NAT_1:45;
card k,k are_equipotent by CARD_1:def 5;
then consider f being Function such that
A6: f is one-to-one and
A7: dom f = card k and
A8: rng f = k by WELLORD2:def 4;
reconsider f = f as Function of (card k),k by A7, A8, FUNCT_2:3;
A9: ( f is onto & f is one-to-one ) by A6, A8, FUNCT_2:def 3;
consider F being XFinSequence of NAT such that
A10: dom F = card k and
A11: card { g where g is Function of (n + 1),k : S₁[g] } = Sum F and
A12: for i being Nat st i in dom F holds
F . i = card { g where g is Function of (n + 1),k : ( S₁[g] & g . n = f . i ) } from STIRL2_1:sch 7(A9, A3, A5);
A14: for i being Nat st i in dom F holds
F . i = n block k

proof

set F2 = { g where g is Function of n,k : ( g is onto & g is "increasing ) } ;
let i be Nat; :: thesis: ( i in dom F implies F . i = n block k )
assume A15: i in dom F ; :: thesis: F . i = n block k
A16: f . i in rng f by A7, A10, A15, FUNCT_1:def 5;
k is Subset of NAT by Th8;
then reconsider fi = f . i as Element of NAT by A8, A16;
A17: fi < k by A16, NAT_1:45;
set F1 = { g where g is Function of (n + 1),k : ( S₁[g] & g . n = fi ) } ;
set F = { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } ;
A18: { g where g is Function of (n + 1),k : ( S₁[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 ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of (n + 1),k : ( S₁[g] & g . n = fi ) } or x in { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } )
assume x in { g where g is Function of (n + 1),k : ( S₁[g] & g . n = fi ) } ; :: thesis: x in { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) }
then ex g being Function of (n + 1),k st
( x = g & S₁[g] & g . n = fi ) ;
hence x in { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } ; :: thesis: verum

end;

{ 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 : ( S₁[g] & g . n = fi ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } or x in { g where g is Function of (n + 1),k : ( S₁[g] & g . n = fi ) } )
assume x in { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} & g . n = fi ) } ; :: thesis: x in { g where g is Function of (n + 1),k : ( S₁[g] & g . n = fi ) }
then ex g being Function of (n + 1),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 (n + 1),k : ( S₁[g] & g . n = fi ) } ; :: thesis: verum

end;

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 : ( S₁[g] & g . n = fi ) } by A18, XBOOLE_0:def 10;
then card { g where g is Function of (n + 1),k : ( S₁[g] & g . n = fi ) } = card { g where g is Function of n,k : ( g is onto & g is "increasing ) } by A17, Th43;
hence F . i = n block k by A12, A15; :: thesis: verum

end;

then for i being Nat st i in dom F holds
F . i <= n block k ;
then A19: Sum F <= (len F) * (n block k) by AFINSQ_2:71;
set G = { g where g is Function of (n + 1),k : S₁[g] } ;
A20: { 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 : S₁[g] }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } or x in { g where g is Function of (n + 1),k : S₁[g] } )
assume x in { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } ; :: thesis: x in { g where g is Function of (n + 1),k : S₁[g] }
then ex g being Function of (n + 1),k st
( x = g & g is onto & g is "increasing & g " {(g . n)} <> {n} ) ;
hence x in { g where g is Function of (n + 1),k : S₁[g] } ; :: thesis: verum

end;

A21: { g where g is Function of (n + 1),k : S₁[g] } c= { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of (n + 1),k : S₁[g] } or x in { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) } )
assume x in { g where g is Function of (n + 1),k : S₁[g] } ; :: thesis: x in { g where g is Function of (n + 1),k : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) }
then ex g being Function of (n + 1),k st
( x = g & S₁[g] ) ;
hence x in { g where g is Function of (n + 1),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 A14;
then A22: Sum F >= (len F) * (n block k) by AFINSQ_2:72;
card k = k by CARD_1:def 5;
then Sum F = k * (n block k) by A10, A19, A22, XXREAL_0:1;
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 A11, A20, A21, XBOOLE_0:def 10; :: thesis: verum

end;

end;

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