let T be non empty 1-sorted ; :: thesis: for S being SetSequence of the carrier of T
for R being subsequence of S
for n being Element of NAT ex m being Element of NAT st
( m >= n & R . n = S . m )
let S be SetSequence of the carrier of T; :: thesis: for R being subsequence of S
for n being Element of NAT ex m being Element of NAT st
( m >= n & R . n = S . m )
let R be subsequence of S; :: thesis: for n being Element of NAT ex m being Element of NAT st
( m >= n & R . n = S . m )
let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( m >= n & R . n = S . m )
consider NS being increasing sequence of NAT such that
A1: R = S * NS by VALUED_0:def 17;
take m = NS . n; :: thesis: ( m >= n & R . n = S . m )
thus m >= n by SEQM_3:33; :: thesis: R . n = S . m
n in NAT ;
then n in dom NS by FUNCT_2:def 1;
hence R . n = S . m by A1, FUNCT_1:23; :: thesis: verum