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

proof

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;

( n = 0 iff n = 0 ) ;
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