let n be Nat; :: thesis: ( n <> 0 implies n block 0 = 0 )

set F = { f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } ;

assume A1: n <> 0 ; :: thesis: n block 0 = 0

{ f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } = {}

set F = { f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } ;

assume A1: n <> 0 ; :: thesis: n block 0 = 0

{ f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } = {}

proof

hence
n block 0 = 0
; :: thesis: verum
assume
{ f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } <> {}
; :: thesis: contradiction

then consider x being object such that

A2: x in { f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } by XBOOLE_0:def 1;

ex f being Function of (Segm n),(Segm 0) st

( x = f & f is onto & f is "increasing ) by A2;

hence contradiction by A1; :: thesis: verum

end;then consider x being object such that

A2: x in { f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } by XBOOLE_0:def 1;

ex f being Function of (Segm n),(Segm 0) st

( x = f & f is onto & f is "increasing ) by A2;

hence contradiction by A1; :: thesis: verum