let i be Nat; :: thesis: for f being FinSequence
for g being complex-valued FinSequence
for o1, o2 being DoubleReorganization of dom g st o1 is valued_reorganization of f & o2 is valued_reorganization of f & rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
(Sum (g *. o1)) . i = (Sum (g *. o2)) . i
let f be FinSequence; :: thesis: for g being complex-valued FinSequence
for o1, o2 being DoubleReorganization of dom g st o1 is valued_reorganization of f & o2 is valued_reorganization of f & rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
(Sum (g *. o1)) . i = (Sum (g *. o2)) . i
let g be complex-valued FinSequence; :: thesis: for o1, o2 being DoubleReorganization of dom g st o1 is valued_reorganization of f & o2 is valued_reorganization of f & rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
(Sum (g *. o1)) . i = (Sum (g *. o2)) . i
let o1, o2 be DoubleReorganization of dom g; :: thesis: ( o1 is valued_reorganization of f & o2 is valued_reorganization of f & rng ((f *. o1) . i) = rng ((f *. o2) . i) implies (Sum (g *. o1)) . i = (Sum (g *. o2)) . i )
assume A1: ( o1 is valued_reorganization of f & o2 is valued_reorganization of f & rng ((f *. o1) . i) = rng ((f *. o2) . i) ) ; :: thesis: (Sum (g *. o1)) . i = (Sum (g *. o2)) . i
A2: rng (o1 . i) = rng (o2 . i) by A1, Lm7;
then consider h being Function such that
A3: ( dom h = dom (o1 . i) & rng h = dom (o2 . i) & h is one-to-one & (o2 . i) * h = o1 . i ) by RFINSEQ:26, CLASSES1:77;
rng ((g *. o1) . i) c= COMPLEX ;
then reconsider g1 = (g *. o1) . i as FinSequence of COMPLEX by FINSEQ_1:def 4;
rng ((g *. o2) . i) c= COMPLEX ;
then reconsider g2 = (g *. o2) . i as FinSequence of COMPLEX by FINSEQ_1:def 4;
len (o1 . i) = len (o2 . i) by A2, FINSEQ_1:48;
then A4: dom (o1 . i) = dom (o2 . i) by FINSEQ_3:29;
A5: len ((g *. o2) . i) = len (o2 . i) by CARD_1:def 7;
then dom g2 = dom (o2 . i) by FINSEQ_3:29;
then reconsider h = h as Function of (dom g2),(dom g2) by A3, A4, FUNCT_2:1;
h is onto by A3, A5, FINSEQ_3:29, FUNCT_2:def 3;
then reconsider h = h as Permutation of (dom g2) by A3;
A6: g1 = g * (o1 . i) by Th41
.= (g * (o2 . i)) * h by A3, RELAT_1:36
.= g2 * h by Th41 ;
thus (Sum (g *. o1)) . i = Sum ((g *. o1) . i) by Def8
.= addcomplex "**" g1 by RVSUM_1:def 11
.= addcomplex "**" g2 by A6, FINSOP_1:7
.= Sum ((g *. o2) . i) by RVSUM_1:def 11
.= (Sum (g *. o2)) . i by Def8 ; :: thesis: verum