let X be set ; :: thesis: for s being sequence of X
for s1 being subsequence of s holds rng s1 c= rng s
let s be sequence of X; :: thesis: for s1 being subsequence of s holds rng s1 c= rng s
let s1 be subsequence of s; :: thesis: rng s1 c= rng s

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

suppose X = {} ; :: thesis: rng s1 c= rng s

hence rng s1 c= rng s ; :: thesis: verum

end;

suppose S: X <> {} ; :: thesis: rng s1 c= rng s

consider N being increasing sequence of NAT such that
A1: s1 = s * N by Def17;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s1 or x in rng s )
assume x in rng s1 ; :: thesis: x in rng s
then consider n being set such that
W1: n in NAT and
W2: x = s1 . n by FUNCT_2:17;
X: N . n in NAT by W1, FUNCT_2:7;
x = s . (N . n) by W1, A1, W2, FUNCT_2:21;
hence x in rng s by X, S, FUNCT_2:6; :: thesis: verum

end;

end;