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