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

proof

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

end;

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