let p, q be XFinSequence; :: thesis: ( p c= q implies ex r being XFinSequence st p ^ r = q )
assume A1: p c= q ; :: thesis: ex r being XFinSequence st p ^ r = q
take r = q /^ (len p); :: thesis: p ^ r = q
thus p ^ r = q by A1, Th77; :: thesis: verum