let K be Field; :: thesis:
let g be FinSequence of K; :: thesis:
let A be set ; :: thesis:
assume A1: A c= dom g ; :: thesis:
A2: ( dom g = Seg (len g) & (dom g) \ A c= dom g ) by FINSEQ_1:def 3, XBOOLE_1:36;
then A3: ( rng (Sgm A) = A & rng (Sgm ((dom g) \ A)) = (dom g) \ A ) by A1, FINSEQ_1:def 13;
then reconsider ga = g * (Sgm A), gb = g * (Sgm ((dom g) \ A)) as FinSequence by A1, A2, FINSEQ_1:20;
( rng ga c= rng g & rng gb c= rng g & rng g c= the carrier of K ) by FINSEQ_1:def 4, RELAT_1:45;
then ( rng ga c= the carrier of K & rng gb c= the carrier of K ) by XBOOLE_1:1;
then reconsider ga = ga, gb = gb as FinSequence of K by FINSEQ_1:def 4;
take ga ; :: thesis:
take gb ; :: thesis:
( (idseq (len g)) " A = A & (idseq (len g)) " ((dom g) \ A) = (dom g) \ A & dom g = rng (idseq (len g)) & dom g = dom (idseq (len g)) ) by A1, A2, FUNCT_2:171, RELAT_1:71;
then A4: (Sgm A) ^ (Sgm ((dom g) \ A)) is Permutation of (dom g) by FINSEQ_3:123;
then reconsider gS = g * ((Sgm A) ^ (Sgm ((dom g) \ A))) as FinSequence of K by A2, FINSEQ_2:50;
set Ad = the addF of K;
A5: ( the addF of K is commutative & the addF of K is associative & the addF of K is having_a_unity ) by FVSUM_1:10;
then the addF of K $$ g = the addF of K "**" gS by A4, FINSOP_1:8
.= the addF of K "**" (ga ^ gb) by A1, A2, A3, Th5
.= (Sum ga) + (Sum gb) by A5, FINSOP_1:6 ;
hence ( ga = g * (Sgm A) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) ) ; :: thesis: