:: deftheorem defines 'not' MODELC_2:def 3 :
for p being FinSequence of NAT holds 'not' p = <*0*> ^ p;