:: deftheorem Def3 defines +^ REWRITE2:def 3 :
for s being XFinSequence
for p, b₃ being XFinSequence-yielding Function holds
( b₃ = p +^ s iff ( dom b₃ = dom p & ( for x being set st x in dom p holds
b₃ . x = (p . x) ^ s ) ) );