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