let S be non empty doubleLoopStr ; :: thesis: for F being non empty Subset of S
for lc being non empty RightLinearCombination of F ex p being RightLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is RightLinearCombination of F )
let F be non empty Subset of S; :: thesis: for lc being non empty RightLinearCombination of F ex p being RightLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is RightLinearCombination of F )
let lc be non empty RightLinearCombination of F; :: thesis: ex p being RightLinearCombination of F ex e being Element of S st
( lc = p ^ <*e*> & <*e*> is RightLinearCombination 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 = a * u
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 = a * u )
assume A2: i in dom p ; :: thesis: ex u being Element of S ex a being Element of F st p /. i = a * u
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 = a * u by A2, Def10;
take u = u; :: thesis: ex a being Element of F st p /. i = a * u
take a = a; :: thesis: p /. i = a * u
thus p /. i = p . i by A2, PARTFUN1:def 6
.= lc . i1 by A1, A2, FINSEQ_1:def 7
.= a * u by A2, A3, A4, PARTFUN1:def 6 ; :: thesis: verum
end;
then reconsider p = p as RightLinearCombination of F by Def10;
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 RightLinearCombination of F )
take e ; :: thesis: ( lc = p ^ <*e*> & <*e*> is RightLinearCombination of F )
thus lc = p ^ <*e*> by A1; :: thesis: <*e*> is RightLinearCombination of F
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 = a * u )
assume A6: i in dom <*e*> ; :: thesis: ex u being Element of S ex a being Element of F st <*e*> /. i = a * u
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) = a * u by A7, Def10;
take u ; :: thesis: ex a being Element of F st <*e*> /. i = a * u
take a ; :: thesis: <*e*> /. i = a * u
thus <*e*> /. i = <*e*> . i by A6, PARTFUN1:def 6
.= e by A9, FINSEQ_1:40
.= a * u by A1, A5, A10, A8, FINSEQ_1:42 ; :: thesis: verum