let XX be non empty set ; :: thesis: for ss1, ss2, ss3 being sequence of XX st ss1 is subsequence of ss2 & ss2 is subsequence of ss3 holds
ss1 is subsequence of ss3
let ss1, ss2, ss3 be sequence of XX; :: thesis: ( ss1 is subsequence of ss2 & ss2 is subsequence of ss3 implies ss1 is subsequence of ss3 )
given N1 being increasing sequence of NAT such that A1: ss1 = ss2 * N1 ; :: according to VALUED_0:def 17 :: thesis: ( not ss2 is subsequence of ss3 or ss1 is subsequence of ss3 )
given N2 being increasing sequence of NAT such that A2: ss2 = ss3 * N2 ; :: according to VALUED_0:def 17 :: thesis: ss1 is subsequence of ss3
take N2 * N1 ; :: according to VALUED_0:def 17 :: thesis: ss1 = ss3 * (N2 * N1)
thus ss1 = ss3 * (N2 * N1) by A1, A2, RELAT_1:36; :: thesis: verum