let n be Nat; :: thesis: ( n block 0 = 1 iff n = 0 )

( n block 0 = 1 implies n = 0 )

( n block 0 = 1 implies n = 0 )

proof

hence
( n block 0 = 1 iff n = 0 )
by Th26; :: thesis: verum
set F = { f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } ;

A1: card {{}} = 1 by CARD_1:30;

assume n block 0 = 1 ; :: thesis: n = 0

then consider x being object such that

A2: { f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } = {x} by A1, CARD_1:29;

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

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

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

hence n = 0 ; :: thesis: verum

end;A1: card {{}} = 1 by CARD_1:30;

assume n block 0 = 1 ; :: thesis: n = 0

then consider x being object such that

A2: { f where f is Function of (Segm n),(Segm 0) : ( f is onto & f is "increasing ) } = {x} by A1, CARD_1:29;

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

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

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

hence n = 0 ; :: thesis: verum