let X be set ; :: thesis: for cf, cf1 being complex-valued FinSubsequence
for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))
let cf, cf1 be complex-valued FinSubsequence; :: thesis: for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))
rng (Seq (cf | X)) c= COMPLEX by VALUED_0:def 1;
then reconsider SfX = Seq (cf | X) as FinSequence of COMPLEX by FINSEQ_1:def 4;
let P be Permutation of (dom cf); :: thesis: ( cf1 = cf * P implies Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X))) )
assume A1: cf1 = cf * P ; :: thesis: Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))
consider Q being Permutation of (dom (Seq (cf1 | (P " X)))) such that
A2: Seq (cf | X) = (Seq (cf1 | (P " X))) * Q by A1, Th9;
rng (Seq (cf1 | (P " X))) c= COMPLEX by VALUED_0:def 1;
then reconsider SfPX = Seq (cf1 | (P " X)) as FinSequence of COMPLEX by FINSEQ_1:def 4;
thus Sum (Seq (cf1 | (P " X))) = addcomplex "**" SfPX by RVSUM_1:def 11
.= addcomplex "**" SfX by A2, FINSOP_1:7
.= Sum (Seq (cf | X)) by RVSUM_1:def 11 ; :: thesis: verum