let XX be non empty set ; :: thesis: for ss being sequence of XX
for ss1 being subsequence of ss holds rng ss1 c= rng ss
let ss be sequence of XX; :: thesis: for ss1 being subsequence of ss holds rng ss1 c= rng ss
let ss1 be subsequence of ss; :: thesis: rng ss1 c= rng ss

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

suppose XX = {} ; :: thesis: rng ss1 c= rng ss

hence rng ss1 c= rng ss ; :: thesis: verum

end;

suppose XX <> {} ; :: thesis: rng ss1 c= rng ss

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ss1 or x in rng ss )
consider N being increasing sequence of NAT such that
A2: ss1 = ss * N by Def17;
assume x in rng ss1 ; :: thesis: x in rng ss
then consider n being set such that
A3: n in NAT and
A4: x = ss1 . n by FUNCT_2:11;
A5: N . n in NAT by A3, FUNCT_2:5;
x = ss . (N . n) by A2, A3, A4, FUNCT_2:15;
hence x in rng ss by A5, FUNCT_2:4; :: thesis: verum

end;

end;