:: deftheorem defines EU MODELC_1:def 11 :
for p, q being FinSequence of NAT holds p EU q = (<*4*> ^ p) ^ q;