theorem :: FINSEQ_6:107

for D being non empty set
for f being trivial FinSequence of D holds
( f is empty or ex x being Element of D st f = <*x*> )