theorem Th1: :: JORDAN1G:1

for f being trivial FinSequence holds
( f is empty or ex x being object st f = <*x*> )