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