let T be non empty 1-sorted ; :: thesis: for S being sequence of T
for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
not S . m in A
let S be sequence of T; :: thesis: for A being Subset of T st ( for S1 being subsequence of S holds not rng S1 c= A ) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
not S . m in A
let A be Subset of T; :: thesis: ( ( for S1 being subsequence of S holds not rng S1 c= A ) implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
not S . m in A )
assume A1: for S1 being subsequence of S holds not rng S1 c= A ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
not S . m in A
defpred S1[ set ] means $1 in A;
assume for n being Element of NAT ex m being Element of NAT st
( n <= m & S . m in A ) ; :: thesis: contradiction
then A2: for n being Element of NAT ex m being Element of NAT st
( n <= m & S1[S . m] ) ;
consider S1 being subsequence of S such that
A3: for n being Element of NAT holds S1[S1 . n] from VALUED_1:sch 1(A2);
 rng S1 c= A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng S1 or y in A )
assume y in rng S1 ; :: thesis: y in A
then consider x1 being object such that
A4: x1 in dom S1 and
A5: S1 . x1 = y by FUNCT_1:def 3;
reconsider n = x1 as Element of NAT by A4;
S1 . n in A by A3;
hence y in A by A5; :: thesis: verum
end;
hence contradiction by A1; :: thesis: verum