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} ) } 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: verumper cases
( k = 0 or k > 0 )
;

end;

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

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;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

card F1 = (n + 1) block k
;
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;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

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

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_{1}[ 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_{1}[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_{1}[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

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_{1}[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_{1}[g] }
_{1}[g] } c= { g where g is Function of (Segm (n + 1)),(Segm k) : ( g is onto & g is "increasing & g " {(g . n)} <> {n} ) }

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;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

( 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

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

A12: for i being Nat st i in dom F holds

F . i = n block k

proof

then
for i being Nat st i in dom F holds
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_{1}[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_{1}[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 ) }
_{1}[g] & g . n = fi ) }
_{1}[g] & g . n = fi ) }
by A16;

then card { g where g is Function of (Segm (n + 1)),(Segm k) : ( S_{1}[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;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

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

proof

{ 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
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_{1}[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_{1}[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_{1}[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;assume x in { g where g is Function of (Segm (n + 1)),(Segm k) : ( S

then ex g being Function of (Segm (n + 1)),(Segm k) st

( x = g & S

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

proof

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
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_{1}[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_{1}[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_{1}[g] & g . n = fi ) }
; :: thesis: verum

end;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

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

then card { g where g is Function of (Segm (n + 1)),(Segm k) : ( S

hence F . i = n block k by A11, A13; :: thesis: verum

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

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

proof

A19:
{ g where g is Function of (Segm (n + 1)),(Segm k) : S
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_{1}[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_{1}[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_{1}[g] }
; :: thesis: verum

end;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

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

proof

for i being Nat st i in dom F holds
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_{1}[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_{1}[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_{1}[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;assume x in { g where g is Function of (Segm (n + 1)),(Segm k) : S

then ex g being Function of (Segm (n + 1)),(Segm k) st

( x = g & S

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

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