let f, g be FinSequence; :: thesis: ( f ^' g is constant implies f is constant )
assume f ^' g is constant ; :: thesis: f is constant
then reconsider h = f ^' g as constant FinSequence ;
rng f c= rng h by TOPREAL8:10;
hence f is constant ; :: thesis: verum