:: deftheorem defines EX MODELC_1:def 9 :
for p being FinSequence of NAT holds EX p = <*2*> ^ p;