for n being Nat st n >= 1 holds
1* n <> 0* n