:: deftheorem Def16 defines exp ORDINAL2:def 16 :
for A, B, b₃ being Ordinal holds
( b₃ = exp (A,B) iff ex fi being Ordinal-Sequence st
( b₃ = last fi & dom fi = succ B & fi . 0 = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> 0 & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) );