let K be Field; :: thesis:
let g be FinSequence of K; :: thesis:
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)) ) by RELAT_1:45;
let A be set ; :: thesis:
assume A4: A c= dom g ; :: thesis:
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, XBOOLE_1:1;
rng gb c= rng g by RELAT_1:26;
then rng gb c= the carrier of K by A1, XBOOLE_1:1;
then reconsider ga = ga, gb = gb as FinSequence of K by A10, FINSEQ_1:def 4;
take ga ; :: thesis:
take gb ; :: thesis:
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: