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