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