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