let K be Field; :: thesis: for g being FinSequence of K

for A being set st A c= dom g holds

ex ga, gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

let g be FinSequence of K; :: thesis: for A being set st A c= dom g holds

ex ga, gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

A1: rng g c= the carrier of K by FINSEQ_1:def 4;

set Ad = the addF of K;

A2: dom g = Seg (len g) by FINSEQ_1:def 3;

then A3: ( dom g = rng (idseq (len g)) & dom g = dom (idseq (len g)) ) ;

let A be set ; :: thesis: ( A c= dom g implies ex ga, gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) ) )

assume A4: A c= dom g ; :: thesis: ex ga, gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

A5: rng (Sgm A) = A by A4, A2, FINSEQ_1:def 13;

A6: (idseq (len g)) " A = A by A4, A2, FUNCT_2:94;

A7: (dom g) \ A c= dom g by XBOOLE_1:36;

then A8: rng (Sgm ((dom g) \ A)) = (dom g) \ A by A2, FINSEQ_1:def 13;

then reconsider ga = g * (Sgm A), gb = g * (Sgm ((dom g) \ A)) as FinSequence by A4, A5, FINSEQ_1:16, XBOOLE_1:36;

(idseq (len g)) " ((dom g) \ A) = (dom g) \ A by A2, A7, FUNCT_2:94;

then A9: (Sgm A) ^ (Sgm ((dom g) \ A)) is Permutation of (dom g) by A6, A3, FINSEQ_3:114;

then reconsider gS = g * ((Sgm A) ^ (Sgm ((dom g) \ A))) as FinSequence of K by A2, FINSEQ_2:46;

rng ga c= rng g by RELAT_1:26;

then A10: rng ga c= the carrier of K by A1;

rng gb c= rng g by RELAT_1:26;

then rng gb c= the carrier of K by A1;

then reconsider ga = ga, gb = gb as FinSequence of K by A10, FINSEQ_1:def 4;

take ga ; :: thesis: ex gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

take gb ; :: thesis: ( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

the addF of K $$ g = the addF of K "**" gS by A9, FINSOP_1:7, FVSUM_1:8

.= the addF of K "**" (ga ^ gb) by A4, A7, A5, A8, Th5

.= (Sum ga) + (Sum gb) by FINSOP_1:5, FVSUM_1:8 ;

hence ( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) ) ; :: thesis: verum

for A being set st A c= dom g holds

ex ga, gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

let g be FinSequence of K; :: thesis: for A being set st A c= dom g holds

ex ga, gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

A1: rng g c= the carrier of K by FINSEQ_1:def 4;

set Ad = the addF of K;

A2: dom g = Seg (len g) by FINSEQ_1:def 3;

then A3: ( dom g = rng (idseq (len g)) & dom g = dom (idseq (len g)) ) ;

let A be set ; :: thesis: ( A c= dom g implies ex ga, gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) ) )

assume A4: A c= dom g ; :: thesis: ex ga, gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

A5: rng (Sgm A) = A by A4, A2, FINSEQ_1:def 13;

A6: (idseq (len g)) " A = A by A4, A2, FUNCT_2:94;

A7: (dom g) \ A c= dom g by XBOOLE_1:36;

then A8: rng (Sgm ((dom g) \ A)) = (dom g) \ A by A2, FINSEQ_1:def 13;

then reconsider ga = g * (Sgm A), gb = g * (Sgm ((dom g) \ A)) as FinSequence by A4, A5, FINSEQ_1:16, XBOOLE_1:36;

(idseq (len g)) " ((dom g) \ A) = (dom g) \ A by A2, A7, FUNCT_2:94;

then A9: (Sgm A) ^ (Sgm ((dom g) \ A)) is Permutation of (dom g) by A6, A3, FINSEQ_3:114;

then reconsider gS = g * ((Sgm A) ^ (Sgm ((dom g) \ A))) as FinSequence of K by A2, FINSEQ_2:46;

rng ga c= rng g by RELAT_1:26;

then A10: rng ga c= the carrier of K by A1;

rng gb c= rng g by RELAT_1:26;

then rng gb c= the carrier of K by A1;

then reconsider ga = ga, gb = gb as FinSequence of K by A10, FINSEQ_1:def 4;

take ga ; :: thesis: ex gb being FinSequence of K st

( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

take gb ; :: thesis: ( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

the addF of K $$ g = the addF of K "**" gS by A9, FINSOP_1:7, FVSUM_1:8

.= the addF of K "**" (ga ^ gb) by A4, A7, A5, A8, Th5

.= (Sum ga) + (Sum gb) by FINSOP_1:5, FVSUM_1:8 ;

hence ( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) ) ; :: thesis: verum