for f1, f2 being Sequence holds f1 c= f1 ^ f2