let n be Element of 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 n,0 : ( f is onto & f is "increasing ) } ;
assume n block 0 = 1 ; :: thesis: n = 0
then ( card { f where f is Function of n,0 : ( f is onto & f is "increasing ) } = 1 & card {{} } = 1 ) by CARD_1:50;
then consider x being set such that
A1: { f where f is Function of n,0 : ( f is onto & f is "increasing ) } = {x} by CARD_1:49;
x in { f where f is Function of n,0 : ( f is onto & f is "increasing ) } by A1, TARSKI:def 1;
then consider f being Function of n,0 such that
A2: ( x = f & f is onto & f is "increasing ) ;
thus n = 0 by A2, Def1; :: thesis: verum

end;

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