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:22;

now

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:39;
then consider u being Element of S, a being Element of F such that
A4: lc /. i = u * a by A2, Def10;
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 8
.= lc . i1 by A1, A2, FINSEQ_1:def 7
.= u * a by A2, A3, A4, PARTFUN1:def 8 ; :: thesis: verum

end;

then reconsider p = p as LeftLinearCombination of F by Def10;
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
A5: len lc = (len p) + 1 by A1, FINSEQ_2:19;
A6: len lc in dom lc by FINSEQ_5:6;
then consider u being Element of S, a being Element of F such that
A7: lc /. (len lc) = u * a by Def10;
A8: lc /. (len lc) = lc . (len lc) by A6, PARTFUN1:def 8;
let i be set ; :: according to IDEAL_1:def 10 :: thesis: ( i in dom <*e*> implies ex u being Element of S ex a being Element of F st <*e*> /. i = u * a )
assume A9: i in dom <*e*> ; :: thesis: ex u being Element of S ex a being Element of F st <*e*> /. i = u * a
dom <*e*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then A10: i = 1 by A9, TARSKI:def 1;
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 A9, PARTFUN1:def 8
.= e by A10, FINSEQ_1:57
.= u * a by A1, A5, A7, A8, FINSEQ_1:59 ; :: thesis: verum