theorem Th4: :: HILBERT2:4

for X being set
for f being FinSequence of X st f <> {} holds
ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*>