theorem :: AFINSQ_2:81

for p, q, r being XFinSequence st q c= r holds
p ^ q c= p ^ r