let f, g be FinSequence; :: thesis: ( f ^' g is constant & f . (len f) = g . 1 & f <> {} implies g is constant )
assume that
A1: f ^' g is constant and
A2: f . (len f) = g . 1 and
A3: f <> {} ; :: thesis: g is constant
reconsider h = f ^' g as constant FinSequence by A1;

per cases ( g <> {} or g = {} ) ;

suppose g <> {} ; :: thesis: g is constant

then rng h = (rng f) \/ (rng g) by A2, A3, FINSEQ_6:144;
then rng g c= rng h by XBOOLE_1:7;
hence g is constant ; :: thesis: verum

end;

suppose g = {} ; :: thesis: g is constant

hence g is constant ; :: thesis: verum

end;

end;