:: deftheorem Def6 defines + BHSP_1:def 6 :
for X being non empty addLoopStr
for seq being sequence of X
for x being Point of X
for b₄ being sequence of X holds
( b₄ = seq + x iff for n being Nat holds b₄ . n = (seq . n) + x );