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
A1: p ^ r = q by Th78;
reconsider r = r as XFinSequence of D by A1, AFINSQ_1:31;
take r ; :: thesis: p ^ r = q
thus p ^ r = q by A1; :: thesis: verum