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}

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

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

f in { g where g is Function of (Segm n),(Segm 1) : ( g is onto & g is "increasing ) }
by A1;
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;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

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