theorem :: JORDAN23:26

for f, g being FinSequence st f ^' g is constant & f . (len f) = g . 1 & f <> {} holds
g is constant