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 ;
A6: (idseq (len g)) " A = A by ;
A7: (dom g) \ A c= dom g by XBOOLE_1:36;
then A8: rng (Sgm ((dom g) \ A)) = (dom g) \ A by ;
then reconsider ga = g * (Sgm A), gb = g * (Sgm ((dom g) \ A)) as FinSequence by ;
(idseq (len g)) " ((dom g) \ A) = (dom g) \ A by ;
then A9: (Sgm A) ^ (Sgm ((dom g) \ A)) is Permutation of (dom g) by ;
then reconsider gS = g * ((Sgm A) ^ (Sgm ((dom g) \ A))) as FinSequence of K by ;
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 ;
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
.= the addF of K "**" (ga ^ gb) by A4, A7, A5, A8, Th5
.= (Sum ga) + (Sum gb) by ;
hence ( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) ) ; :: thesis: verum