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 A1: X <> {} ; :: thesis: rng s1 c= rng s

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

end;

end;