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₁ being Element of L ex p being one-to-one FinSequence of I st
( rng p = J & b₁ = the addF of L "**" (# (p,x)) ) by A1; :: thesis: verum