let S be non empty doubleLoopStr ; :: thesis: for F being non empty Subset of S
for lc being non empty LinearCombination of F ex p being LinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LinearCombination of F )
let F be non empty Subset of S; :: thesis: for lc being non empty LinearCombination of F ex p being LinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LinearCombination of F )
let lc be non empty LinearCombination of F; :: thesis: ex p being LinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is LinearCombination 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, v being Element of S ex a being Element of F st p /. i = (u * a) * v

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

end;

then reconsider p = p as LinearCombination of F by Def8;
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 LinearCombination of F )
take e ; :: thesis: ( lc = p ^ <*e*> & <*e*> is LinearCombination of F )
thus lc = p ^ <*e*> by A1; :: thesis: <*e*> is LinearCombination of F
let i be set ; :: according to IDEAL_1:def 8 :: thesis: ( i in dom <*e*> implies ex u, v being Element of S ex a being Element of F st <*e*> /. i = (u * a) * v )
assume A6: i in dom <*e*> ; :: thesis: ex u, v being Element of S ex a being Element of F st <*e*> /. i = (u * a) * v
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, v being Element of S, a being Element of F such that
A10: lc /. (len lc) = (u * a) * v by A7, Def8;
take u ; :: thesis: ex v being Element of S ex a being Element of F st <*e*> /. i = (u * a) * v
take v ; :: thesis: ex a being Element of F st <*e*> /. i = (u * a) * v
take a ; :: thesis: <*e*> /. i = (u * a) * v
thus <*e*> /. i = <*e*> . i by A6, PARTFUN1:def 6
.= e by A9
.= (u * a) * v by A1, A5, A10, A8, FINSEQ_1:42 ; :: thesis: verum