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