let S be non empty doubleLoopStr ; :: thesis:
let F be non empty Subset of S; :: thesis:
let lc be non empty LinearCombination of F; :: thesis:
len lc <> 0 ;
then consider p being FinSequence of the carrier of S, e being Element of S such that
A1: lc = p ^ <*e*> by FINSEQ_2:22;

let i be set ; :: thesis:
assume A2: i in dom p ; :: thesis:
then reconsider i1 = i as Element of NAT ;
A3: dom p c= dom lc by A1, FINSEQ_1:39;
then consider u, v being Element of S, a being Element of F such that
A4: lc /. i = (u * a) * v by A2, Def9;
take u = u; :: thesis:
take v = v; :: thesis:
take a = a; :: thesis:
thus p /. i = p . i by A2, PARTFUN1:def 8
.= lc . i1 by A1, A2, FINSEQ_1:def 7
.= (u * a) * v by A2, A3, A4, PARTFUN1:def 8 ; :: thesis:

end;

then reconsider p = p as LinearCombination of F by Def9;
take p ; :: thesis:
take e ; :: thesis:
thus lc = p ^ <*e*> by A1; :: thesis:
A5: len lc = (len p) + 1 by A1, FINSEQ_2:19;
A6: len lc in dom lc by FINSEQ_5:6;
then consider u, v being Element of S, a being Element of F such that
A7: lc /. (len lc) = (u * a) * v by Def9;
A8: lc /. (len lc) = lc . (len lc) by A6, PARTFUN1:def 8;
let i be set ; :: according to IDEAL_1:def 9 :: thesis:
assume A9: i in dom <*e*> ; :: thesis:
dom <*e*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then A10: i = 1 by A9, TARSKI:def 1;
take u ; :: thesis:
take v ; :: thesis:
take a ; :: thesis:
thus <*e*> /. i = <*e*> . i by A9, PARTFUN1:def 8
.= e by A10, FINSEQ_1:57
.= (u * a) * v by A1, A5, A7, A8, FINSEQ_1:59 ; :: thesis: