reconsider l1 = l1 as Element of IL ;
<*l1*> is FinSequence of IL ;
hence <*l1*> is IL-FinSequence of S by Def34; :: thesis: verum