defpred S1[ Nat] means for f being complex-valued FinSequence
for o being DoubleReorganization of dom f st len f = $1 holds
Sum f = Sum (Sum (f *. o));
A1:
S1[ 0 ]
A8:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A9:
S1[
i]
;
S1[i + 1]
set i1 =
i + 1;
let f be
complex-valued FinSequence;
for o being DoubleReorganization of dom f st len f = i + 1 holds
Sum f = Sum (Sum (f *. o))let o be
DoubleReorganization of
dom f;
( len f = i + 1 implies Sum f = Sum (Sum (f *. o)) )
assume A10:
len f = i + 1
;
Sum f = Sum (Sum (f *. o))
set fo =
f *. o;
A11:
1
<= i + 1
by NAT_1:11;
then A12:
i + 1
in dom f
by A10, FINSEQ_3:25;
Values o = dom f
by Def7;
then consider x,
y being
object such that A13:
(
x in dom o &
y in dom (o . x) &
(o . x) . y = i + 1 )
by A11, A10, FINSEQ_3:25, Th1;
reconsider x =
x,
y =
y as
Nat by A13;
set ox =
o . x;
set rox =
rng (o . x);
A14:
o . x in rng o
by A13, FUNCT_1:def 3;
then A15:
rng (o . x) c= dom f
by RELAT_1:def 19;
set C =
canFS ((rng (o . x)) \ {(i + 1)});
A16:
i + 1
in rng (o . x)
by A13, FUNCT_1:def 3;
A17:
rng (canFS ((rng (o . x)) \ {(i + 1)})) = (rng (o . x)) \ {(i + 1)}
by FUNCT_2:def 3;
A18:
((rng (o . x)) \ {(i + 1)}) \/ {(i + 1)} = rng (o . x)
by ZFMISC_1:116, A16;
A19:
rng <*(i + 1)*> = {(i + 1)}
by FINSEQ_1:38;
then A20:
rng ((canFS ((rng (o . x)) \ {(i + 1)})) ^ <*(i + 1)*>) = rng (o . x)
by A18, A17, FINSEQ_1:31;
(canFS ((rng (o . x)) \ {(i + 1)})) ^ <*(i + 1)*> is
one-to-one
by XBOOLE_1:79, FINSEQ_3:91, A17, A19;
then consider P being
Permutation of
(dom (o . x)) such that A21:
(canFS ((rng (o . x)) \ {(i + 1)})) ^ <*(i + 1)*> = (o . x) * P
by A20, RFINSEQ:26, RFINSEQ:4;
A22:
rng (canFS ((rng (o . x)) \ {(i + 1)})) c= rng (o . x)
by A17;
A23:
rng (canFS ((rng (o . x)) \ {(i + 1)})) c= (dom f) \ {(i + 1)}
by A17, A14, RELAT_1:def 19, XBOOLE_1:33;
A24:
(rng (canFS ((rng (o . x)) \ {(i + 1)}))) \/ ((dom f) \ {(i + 1)}) = (dom f) \ {(i + 1)}
by A17, A15, XBOOLE_1:33, XBOOLE_1:12;
A25:
rng (canFS ((rng (o . x)) \ {(i + 1)})) c= dom f
by A15, A17;
A26:
(rng (canFS ((rng (o . x)) \ {(i + 1)}))) \/ ((dom f) \ (rng (o . x))) =
(rng (canFS ((rng (o . x)) \ {(i + 1)}))) \/ ((dom f) \ ((rng (canFS ((rng (o . x)) \ {(i + 1)}))) \/ {(i + 1)}))
by A17, ZFMISC_1:116, A16
.=
(rng (canFS ((rng (o . x)) \ {(i + 1)}))) \/ (((dom f) \ (rng (canFS ((rng (o . x)) \ {(i + 1)})))) /\ ((dom f) \ {(i + 1)}))
by XBOOLE_1:53
.=
((rng (canFS ((rng (o . x)) \ {(i + 1)}))) \/ ((dom f) \ (rng (canFS ((rng (o . x)) \ {(i + 1)}))))) /\ ((rng (canFS ((rng (o . x)) \ {(i + 1)}))) \/ ((dom f) \ {(i + 1)}))
by XBOOLE_1:24
.=
(dom f) /\ ((dom f) \ {(i + 1)})
by A25, XBOOLE_1:45, A24
.=
(dom f) \ {(i + 1)}
by XBOOLE_1:28
;
dom f = Seg (i + 1)
by A10, FINSEQ_1:def 3;
then A27:
(dom f) \ {(i + 1)} = Seg i
by FINSEQ_1:10;
set fi =
f | i;
A28:
len (f | i) = i
by NAT_1:11, A10, FINSEQ_1:59;
(rng (canFS ((rng (o . x)) \ {(i + 1)}))) /\ (dom f) c= rng (o . x)
by A22;
then reconsider oC =
o +* (
x,
(canFS ((rng (o . x)) \ {(i + 1)}))) as
DoubleReorganization of
dom (f | i) by A27, A13, Th37, A26;
set FO =
(f | i) *. oC;
A29:
dom oC = dom o
by FUNCT_7:30;
then A30:
len oC = len o
by FINSEQ_3:29;
A31:
len ((f | i) *. oC) = len oC
by CARD_1:def 7;
set FOx =
((f | i) *. oC) | x;
consider H being
FinSequence such that A32:
(f | i) *. oC = (((f | i) *. oC) | x) ^ H
by FINSEQ_1:80;
A33:
( 1
<= x &
x <= len o )
by A13, FINSEQ_3:25;
then A34:
len (((f | i) *. oC) | x) = x
by FINSEQ_1:59, A30, A31;
then A35:
dom (((f | i) *. oC) | x) = Seg x
by FINSEQ_1:def 3;
A36:
x in Seg x
by A33;
reconsider x1 =
x - 1 as
Nat by A33;
len (((f | i) *. oC) | x) = x1 + 1
by A33, FINSEQ_1:59, A30, A31;
then A37:
((f | i) *. oC) | x = ((((f | i) *. oC) | x) | x1) ^ <*((((f | i) *. oC) | x) . x)*>
by FINSEQ_3:55;
A38:
x1 <= x1 + 1
by NAT_1:11;
then A39:
(((f | i) *. oC) | x) | x1 = ((f | i) *. oC) | x1
by FINSEQ_1:82;
reconsider H =
H as
FinSequence-yielding complex-functions-valued FinSequence by A32, Th43, Th44;
reconsider FF =
<*(((f | i) *. oC) . x)*>,
FOx1 =
((f | i) *. oC) | x1 as
FinSequence-yielding complex-functions-valued FinSequence ;
Sum (FOx1 ^ FF) = (Sum FOx1) ^ (Sum FF)
by Th46;
then A40:
Sum (Sum (FOx1 ^ FF)) = (Sum (Sum FOx1)) + (Sum (Sum FF))
by RVSUM_2:32;
(f | i) *. oC = (FOx1 ^ FF) ^ H
by A39, A37, A35, A36, FUNCT_1:47, A32;
then A41:
Sum ((f | i) *. oC) = (Sum (FOx1 ^ FF)) ^ (Sum H)
by Th46;
A42:
Sum FF = <*(Sum (((f | i) *. oC) . x))*>
by Th45;
A43:
len (f *. o) = len o
by CARD_1:def 7;
set fox =
(f *. o) | x;
consider h being
FinSequence such that A44:
f *. o = ((f *. o) | x) ^ h
by FINSEQ_1:80;
A45:
len ((f *. o) | x) = x
by A33, FINSEQ_1:59, A43;
then A46:
dom ((f *. o) | x) = Seg x
by FINSEQ_1:def 3;
len ((f *. o) | x) = x1 + 1
by A33, FINSEQ_1:59, A43;
then A47:
(f *. o) | x = (((f *. o) | x) | x1) ^ <*(((f *. o) | x) . x)*>
by FINSEQ_3:55;
A48:
((f *. o) | x) | x1 = (f *. o) | x1
by A38, FINSEQ_1:82;
reconsider h =
h as
FinSequence-yielding complex-functions-valued FinSequence by A44, Th43, Th44;
reconsider ff =
<*((f *. o) . x)*>,
fox1 =
(f *. o) | x1 as
FinSequence-yielding complex-functions-valued FinSequence ;
Sum (fox1 ^ ff) = (Sum fox1) ^ (Sum ff)
by Th46;
then A49:
Sum (Sum (fox1 ^ ff)) = (Sum (Sum fox1)) + (Sum (Sum ff))
by RVSUM_2:32;
f *. o = (fox1 ^ ff) ^ h
by A44, A47, A48, A46, A36, FUNCT_1:47;
then A50:
Sum (f *. o) = (Sum (fox1 ^ ff)) ^ (Sum h)
by Th46;
A51:
Sum ff = <*(Sum ((f *. o) . x))*>
by Th45;
A52:
(
len fox1 = x1 &
len FOx1 = x1 )
by A38, A45, A34, A48, A39, FINSEQ_1:59;
for
i being
Nat st 1
<= i &
i <= x1 holds
fox1 . i = FOx1 . i
proof
let j be
Nat;
( 1 <= j & j <= x1 implies fox1 . j = FOx1 . j )
assume A53:
( 1
<= j &
j <= x1 )
;
fox1 . j = FOx1 . j
then A54:
j < x
by A38, NAT_1:13;
then A55:
j <= len o
by A33, XXREAL_0:2;
then A56:
j in dom o
by A53, FINSEQ_3:25;
A57:
(
(f *. o) . j = f * (o . j) &
((f | i) *. oC) . j = (f | i) * (oC . j) )
by A55, A53, FINSEQ_3:25, A29, FOMODEL2:def 6;
j in Seg x1
by A53;
then A58:
(
fox1 . j = (f *. o) . j &
FOx1 . j = ((f | i) *. oC) . j )
by FUNCT_1:49;
(
o . j in rng o &
rng o c= (dom f) * )
by A56, FUNCT_1:def 3;
then A59:
o . j is
FinSequence of
dom f
by FINSEQ_1:def 11;
not
i + 1
in rng (o . j)
then A61:
rng (o . j) c= Seg i
by A27, A59, FINSEQ_1:def 4, ZFMISC_1:34;
(f | (Seg i)) * (o . j) =
(f * (id (Seg i))) * (o . j)
by RELAT_1:65
.=
f * ((id (Seg i)) * (o . j))
by RELAT_1:36
.=
f * (o . j)
by A61, RELAT_1:53
;
hence
fox1 . j = FOx1 . j
by A57, A54, FUNCT_7:32, A58;
verum
end;
then A62:
fox1 = FOx1
by A52;
A63:
len ((f | i) *. oC) = (len (((f | i) *. oC) | x)) + (len H)
by A32, FINSEQ_1:22;
then A64:
(len (((f | i) *. oC) | x)) + (len H) = (len ((f *. o) | x)) + (len h)
by A44, FINSEQ_1:22, A43, A31, A30;
for
i being
Nat st 1
<= i &
i <= len H holds
H . i = h . i
proof
let j be
Nat;
( 1 <= j & j <= len H implies H . j = h . j )
set jx =
j + x;
assume A65:
( 1
<= j &
j <= len H )
;
H . j = h . j
then
(
j in dom H &
j in dom h )
by A64, A34, A45, FINSEQ_3:25;
then A66:
(
H . j = ((f | i) *. oC) . (j + x) &
h . j = (f *. o) . (j + x) )
by A34, A45, A32, A44, FINSEQ_1:def 7;
j <> 0
by A65;
then A67:
j + x <> x
;
j <= j + x
by NAT_1:11;
then
j + x >= 1
by A65, XXREAL_0:2;
then A68:
j + x in dom o
by A65, A63, A34, A31, A29, XREAL_1:6, FINSEQ_3:25;
then A69:
(
(f *. o) . (j + x) = f * (o . (j + x)) &
((f | i) *. oC) . (j + x) = (f | i) * (oC . (j + x)) )
by A29, FOMODEL2:def 6;
(
o . (j + x) in rng o &
rng o c= (dom f) * )
by A68, FUNCT_1:def 3;
then A70:
o . (j + x) is
FinSequence of
dom f
by FINSEQ_1:def 11;
not
i + 1
in rng (o . (j + x))
then A72:
rng (o . (j + x)) c= Seg i
by A27, A70, FINSEQ_1:def 4, ZFMISC_1:34;
(f | (Seg i)) * (o . (j + x)) =
(f * (id (Seg i))) * (o . (j + x))
by RELAT_1:65
.=
f * ((id (Seg i)) * (o . (j + x)))
by RELAT_1:36
.=
f * (o . (j + x))
by A72, RELAT_1:53
;
hence
H . j = h . j
by A69, A67, FUNCT_7:32, A66;
verum
end;
then A73:
H = h
by A64, A34, A45;
A74:
(
(f *. o) . x = f * (o . x) &
((f | i) *. oC) . x = (f | i) * (oC . x) )
by A13, A29, FOMODEL2:def 6;
A75:
dom (f * (o . x)) = dom (o . x)
by A15, RELAT_1:27;
rng (f * (o . x)) c= COMPLEX
by VALUED_0:def 1;
then reconsider g =
f * (o . x) as
FinSequence of
COMPLEX by FINSEQ_1:def 4;
reconsider PP =
P as
Permutation of
(dom g) by A75;
A76:
dom (o . x) = Seg (len (o . x))
by FINSEQ_1:def 3;
rng P = dom (o . x)
by FUNCT_2:def 3;
then A77:
(
dom ((o . x) * P) = dom P &
rng ((o . x) * P) = rng (o . x) &
dom (g * P) = dom P &
rng (g * P) = rng g )
by A75, RELAT_1:27, RELAT_1:28;
then
g * PP is
FinSequence
by A76, FUNCT_2:52, FINSEQ_1:def 2;
then reconsider G =
g * PP as
FinSequence of
COMPLEX by FINSEQ_1:def 4, A77;
A78:
Sum g =
addcomplex $$ g
by RVSUM_1:def 11
.=
addcomplex "**" G
by FINSOP_1:7
.=
Sum G
by RVSUM_1:def 11
;
reconsider F =
f as
Function of
(dom f),
(rng f) by FUNCT_2:1;
reconsider I1 =
i + 1 as
Element of
dom f by A11, A10, FINSEQ_3:25;
reconsider C1 =
canFS ((rng (o . x)) \ {(i + 1)}) as
FinSequence of
dom f by A25, FINSEQ_1:def 4;
A79:
( not
dom f is
empty & not
rng f is
empty )
by A12, RELAT_1:42;
G = f * ((o . x) * P)
by RELAT_1:36;
then A80:
G = (F * C1) ^ <*(f . (i + 1))*>
by A21, A79, A12, FINSEQOP:8;
(f | i) * (canFS ((rng (o . x)) \ {(i + 1)})) =
(f * (id (Seg i))) * (canFS ((rng (o . x)) \ {(i + 1)}))
by RELAT_1:65
.=
f * ((id (Seg i)) * (canFS ((rng (o . x)) \ {(i + 1)})))
by RELAT_1:36
.=
f * (canFS ((rng (o . x)) \ {(i + 1)}))
by A23, A27, RELAT_1:53
;
then
((f | i) *. oC) . x = f * (canFS ((rng (o . x)) \ {(i + 1)}))
by A74, A13, FUNCT_7:31;
then A81:
Sum ((f *. o) . x) = (Sum (((f | i) *. oC) . x)) + (f . (i + 1))
by A80, RVSUM_2:31, A78, A74;
A82:
Sum (f | i) =
Sum (Sum ((f | i) *. oC))
by A9, A28
.=
((Sum (Sum FOx1)) + (Sum (Sum FF))) + (Sum (Sum H))
by A41, A40, RVSUM_2:32
.=
((Sum (Sum fox1)) + (Sum (((f | i) *. oC) . x))) + (Sum (Sum h))
by A62, A73, A42, RVSUM_2:30
;
A83:
Sum (Sum (f *. o)) =
((Sum (Sum fox1)) + (Sum (Sum ff))) + (Sum (Sum h))
by A49, A50, RVSUM_2:32
.=
((Sum (Sum fox1)) + (Sum ((f *. o) . x))) + (Sum (Sum h))
by A51, RVSUM_2:30
.=
(((Sum (Sum fox1)) + (Sum (((f | i) *. oC) . x))) + (Sum (Sum h))) + (f . (i + 1))
by A81
;
f = (f | i) ^ <*(f . (i + 1))*>
by FINSEQ_3:55, A10;
hence
Sum f = Sum (Sum (f *. o))
by RVSUM_2:31, A83, A82;
verum
end;
A84:
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A8);
let f be complex-valued FinSequence; for o being DoubleReorganization of dom f holds Sum f = Sum (Sum (f *. o))
let o be DoubleReorganization of dom f; Sum f = Sum (Sum (f *. o))
S1[ len f]
by A84;
hence
Sum f = Sum (Sum (f *. o))
; verum