let n be 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 x in { f where f is Function of n,n : ( f is onto & f is "increasing ) } ; :: thesis: x in {(id n)}
then consider f being Function of n,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 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