:: deftheorem defines '&' MODELC_2:def 4 :
for p, q being FinSequence of NAT holds p '&' q = (<*1*> ^ p) ^ q;