:: deftheorem defines 'or' MODELC_2:def 5 :
for p, q being FinSequence of NAT holds p 'or' q = (<*2*> ^ p) ^ q;