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
let x be object ; :: 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
A1: ss1 = ss * N by Def13;
assume x in rng ss1 ; :: thesis: x in rng ss
then consider n being object such that
A2: n in NAT and
A3: x = ss1 . n by FUNCT_2:11;
A4: N . n in NAT by A2, FUNCT_2:5;
x = ss . (N . n) by A1, A2, A3, FUNCT_2:15;
hence x in rng ss by A4, FUNCT_2:4; :: thesis: verum