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

proof

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;

hence ( n block 0 = 1 iff n = 0 ) by Th26; :: thesis: verum