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

proof

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;

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

proof

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;

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

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;

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

proof

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;

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

proof

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;

Funcs ((n + 1),(k + 1)) is finite by FRAENKEL:6;
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