let k, n be Nat; :: thesis: (n + 1) block (k + 1) = ((k + 1) * (n block (k + 1))) + (n block k)

set F = { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } ;

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

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

A1: { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } c= { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

A5: { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } misses { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

then reconsider F1 = { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } , F2 = { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } as finite set by A9, A8;

reconsider k1 = k + 1 as Element of NAT ;

A10: card F2 = k1 * (n block k1) by Th45;

card F1 = n block k by Th42;

hence (n + 1) block (k + 1) = ((k + 1) * (n block (k + 1))) + (n block k) by A4, A5, A10, CARD_2:40; :: thesis: verum

set F = { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } ;

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

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

A1: { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } c= { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

proof

{ f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } c= { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) }
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } or x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } )

assume x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } ; :: thesis: x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

then consider f being Function of (Segm (n + 1)),(Segm (k + 1)) such that

A2: f = x and

A3: ( f is onto & f is "increasing ) ;

( f " {(f . n)} = {n} or f " {(f . n)} <> {n} ) ;

then ( f in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } or f in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ) by A3;

hence x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } by A2, XBOOLE_0:def 3; :: thesis: verum

end;assume x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } ; :: thesis: x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

then consider f being Function of (Segm (n + 1)),(Segm (k + 1)) such that

A2: f = x and

A3: ( f is onto & f is "increasing ) ;

( f " {(f . n)} = {n} or f " {(f . n)} <> {n} ) ;

then ( f in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } or f in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ) by A3;

hence x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } by A2, XBOOLE_0:def 3; :: thesis: verum

proof

then A4:
{ f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } = { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) }
by A1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } or x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } )

assume x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ; :: thesis: x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) }

then ( x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } or x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ) by XBOOLE_0:def 3;

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

( f = x & f is onto & f is "increasing & f " {(f . n)} = {n} ) or ex f being Function of (Segm (n + 1)),(Segm (k + 1)) st

( f = x & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ) ;

hence x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } ; :: thesis: verum

end;assume x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ; :: thesis: x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) }

then ( x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } or x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ) by XBOOLE_0:def 3;

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

( f = x & f is onto & f is "increasing & f " {(f . n)} = {n} ) or ex f being Function of (Segm (n + 1)),(Segm (k + 1)) st

( f = x & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ) ;

hence x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing ) } ; :: thesis: verum

A5: { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } misses { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

proof

A8:
{ f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } c= Funcs ((n + 1),(k + 1))
assume
{ f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } meets { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }
; :: thesis: contradiction

then consider x being object such that

A6: x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } /\ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } by XBOOLE_0:4;

x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } by A6, XBOOLE_0:def 4;

then A7: ex f being Function of (Segm (n + 1)),(Segm (k + 1)) st

( f = x & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ;

x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } by A6, XBOOLE_0:def 4;

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

( f = x & f is onto & f is "increasing & f " {(f . n)} = {n} ) ;

hence contradiction by A7; :: thesis: verum

end;then consider x being object such that

A6: x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } /\ { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } by XBOOLE_0:4;

x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } by A6, XBOOLE_0:def 4;

then A7: ex f being Function of (Segm (n + 1)),(Segm (k + 1)) st

( f = x & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ;

x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } by A6, XBOOLE_0:def 4;

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

( f = x & f is onto & f is "increasing & f " {(f . n)} = {n} ) ;

hence contradiction by A7; :: thesis: verum

proof

A9:
{ f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } c= Funcs ((n + 1),(k + 1))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } or x in Funcs ((n + 1),(k + 1)) )

assume x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ; :: thesis: x in Funcs ((n + 1),(k + 1))

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

( f = x & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ;

hence x in Funcs ((n + 1),(k + 1)) by FUNCT_2:8; :: thesis: verum

end;assume x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ; :: thesis: x in Funcs ((n + 1),(k + 1))

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

( f = x & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ;

hence x in Funcs ((n + 1),(k + 1)) by FUNCT_2:8; :: thesis: verum

proof

Funcs ((n + 1),(k + 1)) is finite
by FRAENKEL:6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } or x in Funcs ((n + 1),(k + 1)) )

assume x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } ; :: thesis: x in Funcs ((n + 1),(k + 1))

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

( f = x & f is onto & f is "increasing & f " {(f . n)} = {n} ) ;

hence x in Funcs ((n + 1),(k + 1)) by FUNCT_2:8; :: thesis: verum

end;assume x in { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } ; :: thesis: x in Funcs ((n + 1),(k + 1))

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

( f = x & f is onto & f is "increasing & f " {(f . n)} = {n} ) ;

hence x in Funcs ((n + 1),(k + 1)) by FUNCT_2:8; :: thesis: verum

then reconsider F1 = { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } , F2 = { f where f is Function of (Segm (n + 1)),(Segm (k + 1)) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } as finite set by A9, A8;

reconsider k1 = k + 1 as Element of NAT ;

A10: card F2 = k1 * (n block k1) by Th45;

card F1 = n block k by Th42;

hence (n + 1) block (k + 1) = ((k + 1) * (n block (k + 1))) + (n block k) by A4, A5, A10, CARD_2:40; :: thesis: verum