:: deftheorem defines EG MODELC_1:def 10 :
for p being FinSequence of NAT holds EG p = <*3*> ^ p;