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 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 Nat ex m being Element of NAT st
( m >= n & R . n = S . m )
let R be subsequence of S; :: thesis: for n being Nat ex m being Element of NAT st
( m >= n & R . n = S . m )
let n be 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;
reconsider m = NS . n as Element of NAT ;
take m ; :: thesis: ( m >= n & R . n = S . m )
thus m >= n by SEQM_3:14; :: thesis: R . n = S . m
n in NAT by ORDINAL1:def 12;
then n in dom NS by FUNCT_2:def 1;
hence R . n = S . m by A1, FUNCT_1:13; :: thesis: verum