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