let k, n be Nat; (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 ;
TARSKI:def 3 ( 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 ) }
;
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;
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 ;
TARSKI:def 3 ( 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} ) }
;
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 ) }
;
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} ) }
;
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;
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))
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))
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; verum