let i be Nat; 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; 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; 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;
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;
( 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 )
;
rng ((f *. o1) . n) c= rng ((f *. o2) . n)
reconsider O1 =
o1 as
odd_organization of
f by A2;
let y be
object ;
TARSKI:def 3 ( not y in rng ((f *. o1) . n) or y in rng ((f *. o2) . n) )
assume A3:
y in rng ((f *. o1) . n)
;
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
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;
verum
end;
let o1, o2 be DoubleReorganization of dom g; ( 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 )
; (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; verum