let n be Element of NAT ; :: thesis: ( n <> 0 implies n block 1 = 1 )
assume n <> 0 ; :: thesis: n block 1 = 1
then ( ( n = 0 implies 1 = 0 ) & ( 1 = 0 implies n = 0 ) & n >= 1 + 0 ) by NAT_1:13;
then consider f being Function of n,1 such that
A1: ( f is onto & f is "increasing ) by Th23;
set F = { g where g is Function of n,1 : ( g is onto & g is "increasing ) } ;
A2: { g where g is Function of n,1 : ( g is onto & g is "increasing ) } c= {f}

proof

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

end;

f in { g where g is Function of n,1 : ( g is onto & g is "increasing ) } by A1;
then { g where g is Function of n,1 : ( g is onto & g is "increasing ) } = {f} by A2, ZFMISC_1:39;
hence n block 1 = 1 by CARD_1:50; :: thesis: verum