let n be Nat; :: thesis: n block n = 1

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

A1: { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } c= {(id n)}

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

A4: ( f is onto & f is "increasing ) by Th23;

f in { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } by A4;

then { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } = {(id n)} by A1, ZFMISC_1:33;

hence n block n = 1 by CARD_1:30; :: thesis: verum

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

A1: { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } c= {(id n)}

proof

( n = 0 iff n = 0 )
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } or x in {(id n)} )

assume x in { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } ; :: thesis: x in {(id n)}

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

A2: x = f and

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

f = id n by A3, Th20;

hence x in {(id n)} by A2, TARSKI:def 1; :: thesis: verum

end;assume x in { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } ; :: thesis: x in {(id n)}

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

A2: x = f and

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

f = id n by A3, Th20;

hence x in {(id n)} by A2, TARSKI:def 1; :: thesis: verum

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

A4: ( f is onto & f is "increasing ) by Th23;

f in { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } by A4;

then { f where f is Function of (Segm n),(Segm n) : ( f is onto & f is "increasing ) } = {(id n)} by A1, ZFMISC_1:33;

hence n block n = 1 by CARD_1:30; :: thesis: verum