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
take id NAT ; :: according to VALUED_0:def 17 :: thesis: ss = ss * (id NAT)
thus ss = ss * (id NAT) by FUNCT_2:17; :: thesis: verum