let D be non empty set ; :: thesis: for p, q being XFinSequence of D st p c= q holds
ex r being XFinSequence of D st p ^ r = q
let p, q be XFinSequence of D; :: thesis: ( p c= q implies ex r being XFinSequence of D st p ^ r = q )
assume p c= q ; :: thesis: ex r being XFinSequence of D st p ^ r = q
then consider r being XFinSequence such that
W: p ^ r = q by Th91;
reconsider r = r as XFinSequence of D by W, AFINSQ_1:34;
take r ; :: thesis: p ^ r = q
thus p ^ r = q by W; :: thesis: verum