let q, p, r be XFinSequence; :: thesis: ( q c= r implies p ^ q c= p ^ r )
assume q c= r ; :: thesis: p ^ q c= p ^ r
then consider s being XFinSequence such that
W: q ^ s = r by Th91;
p ^ q c= (p ^ q) ^ s by AFINSQ_1:78;
hence p ^ q c= p ^ r by W, AFINSQ_1:30; :: thesis: verum