:: deftheorem Def4 defines |^|^ ORDINAL5:def 4 :
for a, b, b₃ being Ordinal holds
( b₃ = a |^|^ b iff ex phi being Ordinal-Sequence st
( b₃ = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );