theorem Th43: :: FINSEQ_6:43

for D being non empty set
for f being FinSequence of D st f <> {} holds
(f /. 1) .. f = 1