let X be set ; :: thesis: for s1, s2, s3 being sequence of X st s1 is subsequence of s2 & s2 is subsequence of s3 holds
s1 is subsequence of s3
let s1, s2, s3 be sequence of X; :: thesis: ( s1 is subsequence of s2 & s2 is subsequence of s3 implies s1 is subsequence of s3 )
given N1 being increasing sequence of NAT such that A1: s1 = s2 * N1 ; :: according to VALUED_0:def 17 :: thesis: ( not s2 is subsequence of s3 or s1 is subsequence of s3 )
given N2 being increasing sequence of NAT such that A2: s2 = s3 * N2 ; :: according to VALUED_0:def 17 :: thesis: s1 is subsequence of s3
take N2 * N1 ; :: according to VALUED_0:def 17 :: thesis: s1 = s3 * (N2 * N1)
thus s1 = s3 * (N2 * N1) by A1, A2, RELAT_1:55; :: thesis: verum