let S be non empty doubleLoopStr ; :: thesis: for F being non empty Subset of S
for lc being non empty LeftLinearCombination of F ex p being LeftLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LeftLinearCombination of F )
let F be non empty Subset of S; :: thesis: for lc being non empty LeftLinearCombination of F ex p being LeftLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LeftLinearCombination of F )
let lc be non empty LeftLinearCombination of F; :: thesis: ex p being LeftLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LeftLinearCombination of F )
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:19;

now :: thesis: for i being set st i in dom p holds
ex u being Element of S ex a being Element of F st p /. i = u * a

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

end;

then reconsider p = p as LeftLinearCombination of F by Def9;
A5: len lc = (len p) + 1 by A1, FINSEQ_2:16;
take p ; :: thesis: ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LeftLinearCombination of F )
take e ; :: thesis: ( lc = p ^ <*e*> & <*e*> is LeftLinearCombination of F )
thus lc = p ^ <*e*> by A1; :: thesis: <*e*> is LeftLinearCombination of F
let i be set ; :: according to IDEAL_1:def 9 :: thesis: ( i in dom <*e*> implies ex u being Element of S ex a being Element of F st <*e*> /. i = u * a )
assume A6: i in dom <*e*> ; :: thesis: ex u being Element of S ex a being Element of F st <*e*> /. i = u * a
A7: len lc in dom lc by FINSEQ_5:6;
then A8: lc /. (len lc) = lc . (len lc) by PARTFUN1:def 6;
dom <*e*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A9: i = 1 by A6, TARSKI:def 1;
consider u being Element of S, a being Element of F such that
A10: lc /. (len lc) = u * a by A7, Def9;
take u ; :: thesis: ex a being Element of F st <*e*> /. i = u * a
take a ; :: thesis: <*e*> /. i = u * a
thus <*e*> /. i = <*e*> . i by A6, PARTFUN1:def 6
.= e by A9
.= u * a by A1, A5, A10, A8, FINSEQ_1:42 ; :: thesis: verum