theorem :: REWRITE1:66

for p, q being FinSequence st p <> {} & q <> {} holds
(len (p $^ q)) + 1 = (len p) + (len q)