let i be Nat; :: thesis: for f being odd-valued FinSequence
for g being complex-valued FinSequence
for o1, o2 being DoubleReorganization of dom g st o1 is odd_organization of f & o2 is odd_organization of f holds
(Sum (g *. o1)) . i = (Sum (g *. o2)) . i
let f be odd-valued FinSequence; :: thesis: for g being complex-valued FinSequence
for o1, o2 being DoubleReorganization of dom g st o1 is odd_organization of f & o2 is odd_organization of f 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 odd_organization of f & o2 is odd_organization of f holds
(Sum (g *. o1)) . i = (Sum (g *. o2)) . i
A1: for n being Nat
for o1, o2 being DoubleReorganization of dom g st o1 is odd_organization of f & o2 is odd_organization of f holds
rng ((f *. o1) . n) c= rng ((f *. o2) . n)

proof

let n be Nat; :: thesis: for o1, o2 being DoubleReorganization of dom g st o1 is odd_organization of f & o2 is odd_organization of f holds
rng ((f *. o1) . n) c= rng ((f *. o2) . n)
let o1, o2 be DoubleReorganization of dom g; :: thesis: ( o1 is odd_organization of f & o2 is odd_organization of f implies rng ((f *. o1) . n) c= rng ((f *. o2) . n) )
assume A2: ( o1 is odd_organization of f & o2 is odd_organization of f ) ; :: thesis: rng ((f *. o1) . n) c= rng ((f *. o2) . n)
reconsider O1 = o1 as odd_organization of f by A2;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((f *. o1) . n) or y in rng ((f *. o2) . n) )
assume A3: y in rng ((f *. o1) . n) ; :: thesis: y in rng ((f *. o2) . n)
then A4: ( rng ((f *. o1) . n) = {(f . (o1 _ (n,1)))} & 1 in dom (o1 . n) ) by FLEXARY1:49, A2;
A5: n in dom o1

proof

assume not n in dom o1 ; :: thesis: contradiction
then o1 . n = {} by FUNCT_1:def 2;
hence contradiction by A3, FLEXARY1:49, A2; :: thesis: verum

end;

then (o1 . n) . 1 in Values o1 by FLEXARY1:1, A4;
then (o1 . n) . 1 in dom f by FLEXARY1:def 7, A2;
then (o1 . n) . 1 in Values o2 by FLEXARY1:def 7, A2;
then consider j, w being object such that
A6: ( j in dom o2 & w in dom (o2 . j) & (o2 . j) . w = (o1 . n) . 1 ) by FLEXARY1:1;
reconsider j = j, w = w as Nat by A6;
A7: (f *. o1) . n = f * (o1 . n) by A5, FOMODEL2:def 6;
len ((f *. O1) . n) = len (o1 . n) by CARD_1:def 7;
then A8: dom ((f *. o1) . n) = dom (o1 . n) by FINSEQ_3:29;
A9: (2 * n) - 1 = f . (o1 _ (n,1)) & ... & (2 * n) - 1 = f . (o1 _ (n,(len (o1 . n)))) by A2, Def4;
A10: 1 <= len (o1 . n) by A4, FINSEQ_3:25;
A11: (2 * j) - 1 = f . (o2 _ (j,1)) & ... & (2 * j) - 1 = f . (o2 _ (j,(len (o2 . j)))) by A2, Def4;
( 1 <= w & w <= len (o2 . j) ) by A6, FINSEQ_3:25;
then (2 * j) - 1 = f . (o2 _ (j,w)) by A11;
then A12: (2 * j) - 1 = (2 * n) - 1 by A6, A10, A9;
then A13: y = f . (o2 _ (n,w)) by A4, A3, TARSKI:def 1, A6;
A14: (f *. o2) _ (n,w) = f . (o2 _ (n,w)) by FLEXARY1:42;
A15: (o2 . n) . w in dom f by A8, A4, A7, FUNCT_1:11, A6, A12;
(f *. o2) . n = f * (o2 . n) by A12, A6, FOMODEL2:def 6;
then w in dom ((f *. o2) . n) by A15, A6, A12, FUNCT_1:11;
hence y in rng ((f *. o2) . n) by FUNCT_1:def 3, A13, A14; :: thesis: verum

end;

let o1, o2 be DoubleReorganization of dom g; :: thesis: ( o1 is odd_organization of f & o2 is odd_organization of f implies (Sum (g *. o1)) . i = (Sum (g *. o2)) . i )
assume A16: ( o1 is odd_organization of f & o2 is odd_organization of f ) ; :: thesis: (Sum (g *. o1)) . i = (Sum (g *. o2)) . i
rng ((f *. o1) . i) = rng ((f *. o2) . i) by A1, A16;
hence (Sum (g *. o1)) . i = (Sum (g *. o2)) . i by A16, FLEXARY1:51; :: thesis: verum