let K be Field; 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; 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 ; ( 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
; 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
; 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
; ( 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) )
; verum