for f1, f2, f3 being FinSequence st f1 c= f2 holds
f3 ^ f1 c= f3 ^ f2