let s1 be subsequence of s; :: thesis: s1 is constant
rng s1 c= rng s by Th21;
hence s1 is constant ; :: thesis: verum