let X be set ; :: thesis: for s being sequence of X holds s is subsequence of s
let s be sequence of X; :: thesis: s is subsequence of s
reconsider N = id NAT as increasing sequence of NAT ;
take N ; :: according to VALUED_0:def 17 :: thesis: s = s * N
thus s = s * N by FUNCT_2:23; :: thesis: verum