let n, k 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 (n + 1),(k + 1) : ( f is onto & f is "increasing ) } ;
set F1 = { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } ;
set F2 = { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ;
A1: { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing ) } c= { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing ) } or x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } )
assume A2: x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing ) } ; :: thesis: x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }
consider f being Function of (n + 1),(k + 1) such that
A3: ( f = x & f is onto & f is "increasing ) by A2;
( f " {(f . n)} = {n} or f " {(f . n)} <> {n} ) ;
then ( f in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } or f in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ) by A3;
hence x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } by A3, XBOOLE_0:def 3; :: thesis: verum

end;

{ f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } c= { f where f is Function of (n + 1),(k + 1) : ( 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 + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } or x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing ) } )
assume A4: x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ; :: thesis: x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing ) }
( x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } or x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ) by A4, XBOOLE_0:def 3;
then ( ex f being Function of (n + 1),(k + 1) st
( f = x & f is onto & f is "increasing & f " {(f . n)} = {n} ) or ex f being Function of (n + 1),(k + 1) st
( f = x & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ) ;
hence x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing ) } ; :: thesis: verum

end;

then A5: { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } \/ { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } = { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing ) } by A1, XBOOLE_0:def 10;
A6: { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } misses { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }

proof

assume { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } meets { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ; :: thesis: contradiction
then consider x being set such that
A7: x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } /\ { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } by XBOOLE_0:4;
( x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } & x in { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } ) by A7, XBOOLE_0:def 4;
then ( ex f being Function of (n + 1),(k + 1) st
( f = x & f is onto & f is "increasing & f " {(f . n)} = {n} ) & ex f being Function of (n + 1),(k + 1) st
( f = x & f is onto & f is "increasing & f " {(f . n)} <> {n} ) ) ;
hence contradiction ; :: thesis: verum

end;

A8: { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } c= Funcs (n + 1),(k + 1)

proof

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

end;

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

proof

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

end;

Funcs (n + 1),(k + 1) is finite by FRAENKEL:16;
then reconsider F1 = { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} = {n} ) } , F2 = { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) } as finite set by A8, A10;
( n in NAT & k in NAT ) by ORDINAL1:def 13;
then ( card F1 = n block k & card F2 = (k + 1) * (n block (k + 1)) & card { f where f is Function of (n + 1),(k + 1) : ( f is onto & f is "increasing ) } = (n + 1) block (k + 1) ) by Th42, Th55;
hence (n + 1) block (k + 1) = ((k + 1) * (n block (k + 1))) + (n block k) by A5, A6, CARD_2:53; :: thesis: verum