let n be Element of NAT ; :: thesis: ( n <> 0 implies n block 0 = 0 )
assume A1: n <> 0 ; :: thesis: n block 0 = 0
set F = { f where f is Function of n,0 : ( f is onto & f is "increasing ) } ;
{ f where f is Function of n,0 : ( f is onto & f is "increasing ) } = {}

proof

assume { f where f is Function of n,0 : ( f is onto & f is "increasing ) } <> {} ; :: thesis: contradiction
then consider x being set such that
A2: x in { f where f is Function of n,0 : ( f is onto & f is "increasing ) } by XBOOLE_0:def 1;
consider f being Function of n,0 such that
A3: ( x = f & f is onto & f is "increasing ) by A2;
thus contradiction by A1, A3, Def1; :: thesis: verum

end;

hence n block 0 = 0 ; :: thesis: verum