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