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