for D being non trivial set
for f being non empty FinSequence of D
for g being non trivial FinSequence of D st g /. 1 = f /. (len f) & ( for i being Nat st 1 <= i & i < len f holds
f /. i <> g /. 1 ) holds
Rotate ((f ^' g),(g /. 1)) = g ^' f