:: deftheorem Def8 defines exp ORDINAL6:def 8 :
for U being Universe
for a being Ordinal st a in U holds
for b₃ being Ordinal-Sequence of U holds
( b₃ = U exp a iff for b being Ordinal of U holds b₃ . b = exp (a,b) );