let f, g be FinSequence; :: thesis: ( f ^ g is constant implies ( f is constant & g is constant ) )
assume f ^ g is constant ; :: thesis: ( f is constant & g is constant )
then reconsider h = f ^ g as constant FinSequence ;
rng f c= rng h by FINSEQ_1:29;
hence f is constant ; :: thesis: g is constant
rng g c= rng h by FINSEQ_1:30;
hence g is constant ; :: thesis: verum