:: deftheorem Def1 defines +^ ORDINAL3:def 1 :
for C being Ordinal
for fi, b₃ being Ordinal-Sequence holds
( b₃ = C +^ fi iff ( dom b₃ = dom fi & ( for A being Ordinal st A in dom fi holds
b₃ . A = C +^ (fi . A) ) ) );