let p, q, 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
A1: q ^ s = r by Th78;
p ^ q c= (p ^ q) ^ s by AFINSQ_1:74;
hence p ^ q c= p ^ r by A1, AFINSQ_1:27; :: thesis: verum