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