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 ;
hence x in {f} by ; :: 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 ;
hence n block 1 = 1 by CARD_1:30; :: thesis: verum