consider p being FinSequence of I such that

A1: ( rng p = J & p is one-to-one ) by Th1;

the addF of L "**" (# (p,x)) is Element of L ;

hence ex b_{1} being Element of L ex p being one-to-one FinSequence of I st

( rng p = J & b_{1} = the addF of L "**" (# (p,x)) )
by A1; :: thesis: verum

A1: ( rng p = J & p is one-to-one ) by Th1;

the addF of L "**" (# (p,x)) is Element of L ;

hence ex b

( rng p = J & b