for p, q being FinSequence st not p is empty holds
(p ^ q) . 1 = p . 1