:: deftheorem defines 'not' ZF_LANG:def 5 :
for p being FinSequence of NAT holds 'not' p = <*2*> ^ p;