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