for p being FinSequence
for n, m being Nat st m <= n holds
(p | n) | m = p | m by Th5, RELAT_1:74;