let n be Element of NAT ; :: thesis: n block n = 1
set F = { f where f is Function of n,n : ( f is onto & f is "increasing ) } ;
A1: { f where f is Function of n,n : ( f is onto & f is "increasing ) } c= {(id n)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of n,n : ( f is onto & f is "increasing ) } or x in {(id n)} )
assume A2: x in { f where f is Function of n,n : ( f is onto & f is "increasing ) } ; :: thesis: x in {(id n)}
consider f being Function of n,n such that
A3: ( x = f & f is onto & f is "increasing ) by A2;
f = id n by A3, Th20;
hence x in {(id n)} by A3, TARSKI:def 1; :: thesis: verum

end;

( ( n = 0 implies n = 0 ) & ( n = 0 implies n = 0 ) & n >= n ) ;
then consider f being Function of n,n such that
A4: ( f is onto & f is "increasing ) by Th23;
f in { f where f is Function of n,n : ( f is onto & f is "increasing ) } by A4;
then { f where f is Function of n,n : ( f is onto & f is "increasing ) } = {(id n)} by A1, ZFMISC_1:39;
hence n block n = 1 by CARD_1:50; :: thesis: verum