theorem Th1: :: SPRECT_1:1

for f, g being FinSequence st f ^ g is constant holds
( f is constant & g is constant )