:: deftheorem Def1 defines -exponent ORDINAL7:def 1 :
for A being Ordinal-Sequence
for b being Ordinal
for b₃ being Ordinal-Sequence holds
( b₃ = b -exponent A iff ( dom b₃ = dom A & ( for a being object st a in dom A holds
b₃ . a = b -exponent (A . a) ) ) );