theorem Th4: :: POLYALG1:4

for D being non empty set
for f being non empty FinSequence of D holds f = <*(f . 1)*> ^ (Del (f,1))