:: Concatenation of Finite Sequences
:: by Rafa{\l} Ziobro
::
:: Received February 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


registration
let a be Real;
let b be non negative Real;
cluster a -' (a + b) -> zero ;
coherence
a -' (a + b) is zero
proof end;
reduce (a + b) -' a to b;
reducibility
(a + b) -' a = b
proof end;
end;

registration
let n, m be Nat;
identify min (m,n) with n /\ m;
correctness
compatibility
min (m,n) = n /\ m;
proof end;
identify n /\ m with min (m,n);
correctness
compatibility
n /\ m = min (m,n);
;
identify n \/ m with max (m,n);
correctness
compatibility
n \/ m = max (m,n);
proof end;
end;

registration
let n, m be non negative Real;
reduce min ((n + m),n) to n;
reducibility
min ((n + m),n) = n
proof end;
reduce max ((n + m),n) to n + m;
reducibility
max ((n + m),n) = n + m
proof end;
end;

theorem CNM: :: RVSUM_4:1
for f being Relation
for n, m being Nat holds (f | (n + m)) | n = f | n
proof end;

theorem CNX: :: RVSUM_4:2
for f being Function
for n being Nat
for m being non zero Nat holds (f | (n + m)) . n = f . n
proof end;

registration
let D be non empty set ;
let x be sequence of D;
let n be Nat;
reduce dom (x | n) to n;
reducibility
dom (x | n) = n
proof end;
cluster x | n -> Sequence-like finite ;
coherence
( x | n is finite & x | n is Sequence-like ) ;
cluster x | n -> n -element ;
coherence
x | n is n -element
proof end;
end;

theorem MFG: :: RVSUM_4:3
for f, g being complex-valued Function
for X being set holds (f (#) g) | X = (f | X) (#) (g | X)
proof end;

registration
let D be non empty set ;
let f, g be sequence of D;
cluster f +* g -> Sequence-like ;
coherence
f +* g is Sequence-like by FUNCT_2:def 1;
end;

registration
let f be constant Complex_Sequence;
let n be Nat;
cluster f ^\ n -> constant ;
coherence
f ^\ n is constant ;
end;

registration
cluster Relation-like empty-yielding omega -defined COMPLEX -valued non empty Function-like V32( omega ) V33( omega , COMPLEX ) complex-valued for Element of K16(K17(omega,COMPLEX));
existence
ex b1 being Complex_Sequence st b1 is empty-yielding
proof end;
cluster Relation-like empty-yielding omega -defined REAL -valued non empty Function-like V32( omega ) V33( omega , REAL ) complex-valued ext-real-valued real-valued for Element of K16(K17(omega,REAL));
existence
ex b1 being Real_Sequence st b1 is empty-yielding
proof end;
cluster empty-yielding Function-like V33( omega , COMPLEX ) -> natural-valued for Element of K16(K17(omega,COMPLEX));
coherence
for b1 being Complex_Sequence st b1 is empty-yielding holds
b1 is natural-valued
proof end;
cluster Relation-like omega -defined COMPLEX -valued non empty Function-like constant V32( omega ) V33( omega , COMPLEX ) complex-valued real-valued for Element of K16(K17(omega,COMPLEX));
existence
ex b1 being Complex_Sequence st
( b1 is constant & b1 is real-valued )
proof end;
end;

:: seq <-> FinSeq in DBLSEQ_2:49 -- etc.
theorem :: RVSUM_4:4
for s being Real_Sequence
for n being Nat holds (Partial_Sums s) . n = Sum (s | (Segm (n + 1))) by AFINSQ_2:56;

definition
let c be Complex;
func seq_const c -> Complex_Sequence equals :: RVSUM_4:def 1
NAT --> c;
coherence
NAT --> c is Complex_Sequence
proof end;
end;

:: deftheorem defines seq_const RVSUM_4:def 1 :
for c being Complex holds seq_const c = NAT --> c;

registration
let c be Complex;
let n be Nat;
reduce (seq_const c) . n to c;
reducibility
(seq_const c) . n = c by ORDINAL1:def 12, FUNCOP_1:7;
end;

theorem SFG: :: RVSUM_4:5
for f, g being complex-valued Function
for X being set holds (f + g) | X = (f | X) + (g | X)
proof end;

registration
let f be 1 -element FinSequence;
reduce <*(f . 1)*> to f;
reducibility
<*(f . 1)*> = f
proof end;
end;

registration
let f be 2 -element FinSequence;
reduce <*(f . 1),(f . 2)*> to f;
reducibility
<*(f . 1),(f . 2)*> = f
proof end;
end;

registration
let f be 3 -element FinSequence;
reduce <*(f . 1),(f . 2),(f . 3)*> to f;
reducibility
<*(f . 1),(f . 2),(f . 3)*> = f
proof end;
end;

theorem :: RVSUM_4:6
for f being complex-valued FinSequence holds Sum f = (f . 1) + (Sum (f /^ 1))
proof end;

theorem FIF: :: RVSUM_4:7
for f being non empty complex-valued FinSequence holds Product f = (f . 1) * (Product (f /^ 1))
proof end;

LmFNK: for n being Nat
for f being b1 + 1 -element FinSequence holds f = (f | n) ^ <*(f . (n + 1))*>
proof end;

theorem FNK: :: RVSUM_4:8
for n being Nat
for m being non zero Nat
for f being b1 + b2 -element FinSequence holds f | (n + 1) = (f | n) ^ <*(f . (n + 1))*>
proof end;

theorem PAP: :: RVSUM_4:9
for f being complex-valued FinSequence
for n being Nat holds Product f = (Product (f | n)) * (Product (f /^ n))
proof end;

theorem FAF: :: RVSUM_4:10
for f, g being complex-valued FinSequence holds Product (f ^ g) = (Product f) * (Product g)
proof end;

:: FINSOP_1 -- +*
definition
let s be Complex_Sequence;
func Partial_Product s -> Complex_Sequence means :PP: :: RVSUM_4:def 2
( it . 0 = s . 0 & ( for n being Nat holds it . (n + 1) = (it . n) * (s . (n + 1)) ) );
existence
ex b1 being Complex_Sequence st
( b1 . 0 = s . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) * (s . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being Complex_Sequence st b1 . 0 = s . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) * (s . (n + 1)) ) & b2 . 0 = s . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) * (s . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem PP defines Partial_Product RVSUM_4:def 2 :
for s, b2 being Complex_Sequence holds
( b2 = Partial_Product s iff ( b2 . 0 = s . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) * (s . (n + 1)) ) ) );

theorem PPN: :: RVSUM_4:11
for f being Complex_Sequence
for n being Nat st f . n = 0 holds
(Partial_Product f) . n = 0
proof end;

theorem PPM: :: RVSUM_4:12
for f being Complex_Sequence
for n, m being Nat st f . n = 0 holds
(Partial_Product f) . (n + m) = 0
proof end;

definition
let c be Complex;
let n be non zero Nat;
redefine func c |^ n equals :: RVSUM_4:def 3
(Partial_Product (seq_const c)) . (n - 1);
compatibility
for b1 being set holds
( b1 = c |^ n iff b1 = (Partial_Product (seq_const c)) . (n - 1) )
proof end;
end;

:: deftheorem defines |^ RVSUM_4:def 3 :
for c being Complex
for n being non zero Nat holds c |^ n = (Partial_Product (seq_const c)) . (n - 1);

theorem COMSEQ324: :: RVSUM_4:13
for n being Nat holds (Partial_Product (seq_const 0c)) . n = 0
proof end;

registration
let k be Nat;
reduce (Partial_Product (seq_const 0)) . k to 0 ;
reducibility
(Partial_Product (seq_const 0)) . k = 0
proof end;
end;

registration
cluster empty-yielding Function-like V33( omega , COMPLEX ) -> absolutely_summable for Element of K16(K17(omega,COMPLEX));
coherence
for b1 being Complex_Sequence st b1 is empty-yielding holds
b1 is absolutely_summable
proof end;
cluster empty-yielding Function-like V33( omega , REAL ) -> absolutely_summable for Element of K16(K17(omega,REAL));
coherence
for b1 being Real_Sequence st b1 is empty-yielding holds
b1 is absolutely_summable
proof end;
end;

registration
reduce Partial_Sums (NAT --> 0) to NAT --> 0;
reducibility
Partial_Sums (NAT --> 0) = NAT --> 0
proof end;
reduce Partial_Product (seq_const 0) to seq_const 0;
reducibility
Partial_Product (seq_const 0) = seq_const 0 by COMSEQ324, PARTFUN1:def 2;
cluster Function-like V33( omega , COMPLEX ) -> Sequence-like for Element of K16(K17(omega,COMPLEX));
coherence
for b1 being Complex_Sequence holds b1 is Sequence-like by COMSEQ_1:1;
cluster Relation-like omega -defined COMPLEX -valued non empty Function-like V32( omega ) V33( omega , COMPLEX ) complex-valued summable for Element of K16(K17(omega,COMPLEX));
existence
ex b1 being sequence of COMPLEX st b1 is summable
proof end;
end;

registration
let seq be empty-yielding Complex_Sequence;
cluster Sum seq -> zero ;
coherence
Sum seq is zero
proof end;
end;

registration
let seq be empty-yielding Real_Sequence;
cluster Sum seq -> zero ;
coherence
Sum seq is zero
proof end;
end;

registration
let c be Complex;
cluster <%c%> -> complex-valued ;
coherence
<%c%> is complex-valued ;
reduce Sum <%c%> to c;
reducibility
Sum <%c%> = c by AFINSQ_2:53;
end;

registration
let n be Nat;
cluster Relation-like omega -defined REAL -valued Sequence-like Function-like finite n -element V61() complex-valued ext-real-valued real-valued natural-valued for set ;
existence
ex b1 being natural-valued XFinSequence st b1 is n -element
proof end;
let k be object ;
cluster n --> k -> n -element ;
coherence
n --> k is n -element
proof end;
end;

registration
let n be Nat;
cluster Relation-like omega -defined Sequence-like Function-like finite n -element V61() for set ;
existence
ex b1 being XFinSequence st b1 is n -element
proof end;
let f be n -element XFinSequence;
reduce f | n to f;
reducibility
f | n = f
proof end;
end;

registration
let n, m be Nat;
let f be n -element XFinSequence;
reduce f | (n + m) to f;
reducibility
f | (n + m) = f
proof end;
end;

registration
let f be 1 -element XFinSequence;
reduce <%(f . 0)%> to f;
reducibility
<%(f . 0)%> = f
proof end;
end;

registration
let f be 2 -element XFinSequence;
reduce <%(f . 0),(f . 1)%> to f;
reducibility
<%(f . 0),(f . 1)%> = f
proof end;
end;

registration
let f be 3 -element XFinSequence;
reduce <%(f . 0),(f . 1),(f . 2)%> to f;
reducibility
<%(f . 0),(f . 1),(f . 2)%> = f
proof end;
end;

:: Segm
theorem LmA: :: RVSUM_4:14
for n, k being Nat st k in Segm (n + 1) holds
n - k is Nat
proof end;

theorem :: RVSUM_4:15
for a, b being Complex
for n, k being Nat st k in Segm (n + 1) holds
ex c being object ex l being Nat st
( l = n - k & c = (a |^ l) * (b |^ k) )
proof end;

:: Extending XFinSequence
definition
let f be complex-valued XFinSequence;
let seq be Complex_Sequence;
func f ^ seq -> Complex_Sequence equals :: RVSUM_4:def 4
f \/ (Shift (seq,(len f)));
correctness
coherence
f \/ (Shift (seq,(len f))) is Complex_Sequence;
proof end;
end;

:: deftheorem defines ^ RVSUM_4:def 4 :
for f being complex-valued XFinSequence
for seq being Complex_Sequence holds f ^ seq = f \/ (Shift (seq,(len f)));

definition
let seq be Complex_Sequence;
let f be Function;
func seq ^ f -> sequence of COMPLEX equals :: RVSUM_4:def 5
seq;
coherence
seq is sequence of COMPLEX ;
end;

:: deftheorem defines ^ RVSUM_4:def 5 :
for seq being Complex_Sequence
for f being Function holds seq ^ f = seq;

theorem RSC: :: RVSUM_4:16
for x being object holds
( x is real-valued Complex_Sequence iff x is Real_Sequence )
proof end;

theorem :: RVSUM_4:17
for rseq being Real_Sequence
for cseq being Complex_Sequence st cseq = rseq holds
Partial_Product rseq = Partial_Product cseq
proof end;

definition
let f be complex-valued XFinSequence;
let seq be Real_Sequence;
func f ^ seq -> Complex_Sequence equals :: RVSUM_4:def 6
f \/ (Shift (seq,(len f)));
correctness
coherence
f \/ (Shift (seq,(len f))) is Complex_Sequence;
proof end;
end;

:: deftheorem defines ^ RVSUM_4:def 6 :
for f being complex-valued XFinSequence
for seq being Real_Sequence holds f ^ seq = f \/ (Shift (seq,(len f)));

theorem :: RVSUM_4:18
for rseq being Real_Sequence holds (<%> REAL) ^ rseq is real-valued Complex_Sequence ;

:: may be used for conversion of Real_Sequences into Complex_Sequences
definition
let f be Real_Sequence;
let g be Function;
func f ^ g -> real-valued sequence of COMPLEX equals :: RVSUM_4:def 7
f;
correctness
coherence
f is real-valued sequence of COMPLEX;
by RSC;
end;

:: deftheorem defines ^ RVSUM_4:def 7 :
for f being Real_Sequence
for g being Function holds f ^ g = f;

registration
let f be complex-valued XFinSequence;
let seq be Complex_Sequence;
reduce (f ^ seq) | (dom f) to f;
reducibility
(f ^ seq) | (dom f) = f
proof end;
end;

registration
let f be complex-valued XFinSequence;
let seq be Real_Sequence;
reduce (f ^ seq) | (dom f) to f;
reducibility
(f ^ seq) | (dom f) = f
proof end;
end;

theorem SCX: :: RVSUM_4:19
for f being complex-valued XFinSequence
for x being Nat holds (f ^ (seq_const 0)) . x = f . x
proof end;

theorem :: RVSUM_4:20
for f being Real_Sequence holds f ^ f is real-valued Complex_Sequence ;

registration
let f be real-valued Complex_Sequence;
cluster Im f -> empty-yielding ;
coherence
Im f is empty-yielding
proof end;
reduce Re f to f;
reducibility
Re f = f
proof end;
end;

registration
cluster Relation-like empty-yielding omega -defined REAL -valued non empty Function-like V32( omega ) V33( omega , REAL ) complex-valued ext-real-valued real-valued for Element of K16(K17(omega,REAL));
existence
ex b1 being Real_Sequence st b1 is empty-yielding
proof end;
cluster Function-like V33( omega , REAL ) -> Sequence-like for Element of K16(K17(omega,REAL));
coherence
for b1 being Real_Sequence holds b1 is Sequence-like by SEQ_1:1;
end;

registration
let r be Real;
cluster Re (r * <i>) -> zero ;
coherence
Re (r * <i>) is zero by COMPLEX1:10;
reduce Im (r * <i>) to r;
reducibility
Im (r * <i>) = r by COMPLEX1:11;
end;

registration
let f be complex-valued XFinSequence;
cluster Re f -> Sequence-like finite real-valued ;
coherence
( Re f is real-valued & Re f is finite & Re f is Sequence-like )
proof end;
cluster Im f -> Sequence-like finite real-valued ;
coherence
( Im f is real-valued & Im f is finite & Im f is Sequence-like )
proof end;
cluster Re f -> len f -element ;
coherence
Re f is len f -element
proof end;
cluster Im f -> len f -element ;
coherence
Im f is len f -element
proof end;
end;

registration
let f be complex-valued FinSequence;
cluster Re f -> FinSequence-like real-valued ;
coherence
( Re f is real-valued & Re f is FinSequence-like )
proof end;
cluster Im f -> FinSequence-like real-valued ;
coherence
( Im f is real-valued & Im f is FinSequence-like )
proof end;
end;

registration
let f be complex-valued Function;
reduce Re (Re f) to Re f;
reducibility
Re (Re f) = Re f
proof end;
reduce Re (Im f) to Im f;
reducibility
Re (Im f) = Im f
proof end;
cluster Im (Re f) -> empty-yielding ;
coherence
Im (Re f) is empty-yielding
proof end;
cluster Im (Im f) -> empty-yielding ;
coherence
Im (Im f) is empty-yielding
proof end;
reduce Re ((Re f) + (<i> (#) (Im f))) to Re f;
reducibility
Re ((Re f) + (<i> (#) (Im f))) = Re f
proof end;
reduce Im ((Re f) + (<i> (#) (Im f))) to Im f;
reducibility
Im ((Re f) + (<i> (#) (Im f))) = Im f
proof end;
reduce (Re f) + (<i> (#) (Im f)) to f;
reducibility
(Re f) + (<i> (#) (Im f)) = f
proof end;
end;

registration
let n be Nat;
cluster Relation-like Function-like finite n -element for set ;
existence
ex b1 being finite Function st b1 is n -element
proof end;
end;

registration
let f be finite complex-valued Sequence;
let n be Nat;
cluster Shift (f,n) -> finite ;
coherence
Shift (f,n) is finite ;
cluster Shift (f,n) -> len f -element ;
coherence
Shift (f,n) is len f -element
proof end;
end;

registration
cluster seq_const 0 -> empty-yielding ;
coherence
seq_const 0 is empty-yielding ;
end;

definition
let f be complex-valued XFinSequence;
func Sequel f -> Complex_Sequence equals :: RVSUM_4:def 8
(NAT --> 0) +* f;
coherence
(NAT --> 0) +* f is Complex_Sequence
proof end;
end;

:: deftheorem defines Sequel RVSUM_4:def 8 :
for f being complex-valued XFinSequence holds Sequel f = (NAT --> 0) +* f;

theorem SFX: :: RVSUM_4:21
for f being complex-valued XFinSequence
for x being Nat holds (Sequel f) . x = f . x
proof end;

theorem :: RVSUM_4:22
for f being complex-valued XFinSequence holds Sequel f = f ^ (seq_const 0)
proof end;

theorem :: RVSUM_4:23
for seq being Complex_Sequence holds seq = (Re seq) + (<i> (#) (Im seq)) ;

theorem RSF: :: RVSUM_4:24
for f being complex-valued XFinSequence holds Re (Sequel f) = Sequel (Re f)
proof end;

theorem ISF: :: RVSUM_4:25
for f being complex-valued XFinSequence holds Im (Sequel f) = Sequel (Im f)
proof end;

theorem :: RVSUM_4:26
for c being Complex holds 0 (#) (NAT --> c) = NAT --> 0
proof end;

theorem FIC: :: RVSUM_4:27
for seq being Complex_Sequence
for x being Nat st ( for k being Nat st k >= x holds
seq . k = 0 ) holds
seq is summable
proof end;

theorem :: RVSUM_4:28
for seq being Real_Sequence
for x being Nat st ( for k being Nat st k >= x holds
seq . k = 0 ) holds
seq is summable
proof end;

registration
let f be complex-valued XFinSequence;
cluster Sequel f -> summable ;
coherence
Sequel f is summable
proof end;
end;

:: Concatenation of (X)FinSequences
definition
let f be XFinSequence;
let g be FinSequence;
func f ^ g -> XFinSequence means :Def1: :: RVSUM_4:def 9
( dom it = (len f) + (len g) & ( for k being Nat st k in dom f holds
it . k = f . k ) & ( for k being Nat st k in dom g holds
it . (((len f) + k) - 1) = g . k ) );
existence
ex b1 being XFinSequence st
( dom b1 = (len f) + (len g) & ( for k being Nat st k in dom f holds
b1 . k = f . k ) & ( for k being Nat st k in dom g holds
b1 . (((len f) + k) - 1) = g . k ) )
proof end;
uniqueness
for b1, b2 being XFinSequence st dom b1 = (len f) + (len g) & ( for k being Nat st k in dom f holds
b1 . k = f . k ) & ( for k being Nat st k in dom g holds
b1 . (((len f) + k) - 1) = g . k ) & dom b2 = (len f) + (len g) & ( for k being Nat st k in dom f holds
b2 . k = f . k ) & ( for k being Nat st k in dom g holds
b2 . (((len f) + k) - 1) = g . k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines ^ RVSUM_4:def 9 :
for f being XFinSequence
for g being FinSequence
for b3 being XFinSequence holds
( b3 = f ^ g iff ( dom b3 = (len f) + (len g) & ( for k being Nat st k in dom f holds
b3 . k = f . k ) & ( for k being Nat st k in dom g holds
b3 . (((len f) + k) - 1) = g . k ) ) );

definition
let f be FinSequence;
let g be XFinSequence;
func f ^ g -> FinSequence means :Def2: :: RVSUM_4:def 10
( dom it = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
it . k = f . k ) & ( for k being Nat st k in dom g holds
it . (((len f) + k) + 1) = g . k ) );
existence
ex b1 being FinSequence st
( dom b1 = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
b1 . k = f . k ) & ( for k being Nat st k in dom g holds
b1 . (((len f) + k) + 1) = g . k ) )
proof end;
uniqueness
for b1, b2 being FinSequence st dom b1 = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
b1 . k = f . k ) & ( for k being Nat st k in dom g holds
b1 . (((len f) + k) + 1) = g . k ) & dom b2 = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
b2 . k = f . k ) & ( for k being Nat st k in dom g holds
b2 . (((len f) + k) + 1) = g . k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ^ RVSUM_4:def 10 :
for f being FinSequence
for g being XFinSequence
for b3 being FinSequence holds
( b3 = f ^ g iff ( dom b3 = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds
b3 . k = f . k ) & ( for k being Nat st k in dom g holds
b3 . (((len f) + k) + 1) = g . k ) ) );

theorem XL1: :: RVSUM_4:29
for f being XFinSequence
for g being FinSequence holds
( len (f ^ g) = (len f) + (len g) & len (g ^ f) = (len f) + (len g) )
proof end;

registration
let n, m be Nat;
let f be n -element XFinSequence;
let g be m -element FinSequence;
cluster f ^ g -> n + m -element ;
coherence
f ^ g is n + m -element
proof end;
cluster g ^ f -> n + m -element ;
coherence
g ^ f is n + m -element
proof end;
end;

theorem XDF: :: RVSUM_4:30
for f being XFinSequence
for g being FinSequence
for x being Nat holds
( x in dom (f ^ g) iff ( x in dom f or (x + 1) - (len f) in dom g ) )
proof end;

theorem FDX: :: RVSUM_4:31
for f being FinSequence
for g being XFinSequence
for x being Nat holds
( x in dom (f ^ g) iff ( x in dom f or x - ((len f) + 1) in dom g ) )
proof end;

theorem FRX: :: RVSUM_4:32
for f being FinSequence
for g being XFinSequence holds
( rng (f ^ g) = (rng f) \/ (rng g) & rng (g ^ f) = (rng f) \/ (rng g) )
proof end;

theorem :: RVSUM_4:33
for f being non empty XFinSequence
for g being FinSequence holds dom (f \/ (Shift (g,((len f) - 1)))) = Segm ((len f) + (len g))
proof end;

theorem :: RVSUM_4:34
for f being FinSequence
for g being XFinSequence holds dom (f \/ (Shift (g,((len f) + 1)))) = Seg ((len f) + (len g))
proof end;

registration
let f be complex-valued FinSequence;
cluster (<%> COMPLEX) ^ f -> complex-valued ;
coherence
(<%> COMPLEX) ^ f is complex-valued
proof end;
end;

registration
let f be complex-valued XFinSequence;
cluster (<*> COMPLEX) ^ f -> complex-valued ;
coherence
(<*> COMPLEX) ^ f is complex-valued
proof end;
end;

registration
let f be XFinSequence;
let g be FinSequence;
reduce (f ^ g) | (len f) to f;
reducibility
(f ^ g) | (len f) = f
proof end;
reduce (g ^ f) | (len g) to g;
reducibility
(g ^ f) | (len g) = g
proof end;
end;

theorem :: RVSUM_4:35
for D being set
for f being XFinSequence
for g being FinSequence of D holds (f ^ g) /^ (len f) = FS2XFS g
proof end;

theorem :: RVSUM_4:36
for f being XFinSequence holds f is XFinSequence of (rng f) \/ {1} by RELAT_1:def 19, XBOOLE_1:7;

theorem :: RVSUM_4:37
for D being set
for f being FinSequence
for g being XFinSequence of D holds (f ^ g) /^ (len f) = XFS2FS g
proof end;

definition
let D be set ;
let f be XFinSequence of D;
:: original: XFS2FS
redefine func XFS2FS f -> FinSequence of D equals :: RVSUM_4:def 11
(<*> D) ^ f;
coherence
XFS2FS f is FinSequence of D
proof end;
compatibility
for b1 being FinSequence of D holds
( b1 = XFS2FS f iff b1 = (<*> D) ^ f )
proof end;
end;

:: deftheorem defines XFS2FS RVSUM_4:def 11 :
for D being set
for f being XFinSequence of D holds XFS2FS f = (<*> D) ^ f;

theorem DSS: :: RVSUM_4:38
for D being set
for f being XFinSequence of D holds dom (Shift (f,1)) = Seg (len f)
proof end;

definition
let D be set ;
let f be XFinSequence of D;
:: original: XFS2FS
redefine func XFS2FS f -> FinSequence of D equals :: RVSUM_4:def 12
 Shift (f,1);
coherence
XFS2FS f is FinSequence of D
proof end;
compatibility
for b1 being FinSequence of D holds
( b1 = XFS2FS f iff b1 = Shift (f,1) )
proof end;
end;

:: deftheorem defines XFS2FS RVSUM_4:def 12 :
for D being set
for f being XFinSequence of D holds XFS2FS f = Shift (f,1);

definition
let D be set ;
let f be FinSequence of D;
redefine func FS2XFS f equals :: RVSUM_4:def 13
(<%> D) ^ f;
compatibility
for b1 being set holds
( b1 = FS2XFS f iff b1 = (<%> D) ^ f )
proof end;
end;

:: deftheorem defines FS2XFS RVSUM_4:def 13 :
for D being set
for f being FinSequence of D holds FS2XFS f = (<%> D) ^ f;

theorem XFX: :: RVSUM_4:39
for D being set
for f, g being XFinSequence of D holds f ^ g = f ^ (XFS2FS g)
proof end;

theorem FXF: :: RVSUM_4:40
for D being set
for f, g being FinSequence of D holds f ^ g = f ^ (FS2XFS g)
proof end;

registration
let f be XFinSequence of REAL ;
reduce (Sequel f) | (dom f) to f;
reducibility
(Sequel f) | (dom f) = f ;
cluster Shift (f,1) -> FinSequence-like ;
coherence
Shift (f,1) is FinSequence-like
proof end;
cluster (Sequel f) ^\ (dom f) -> empty-yielding ;
coherence
(Sequel f) ^\ (dom f) is empty-yielding
proof end;
end;

theorem FFX: :: RVSUM_4:41
for D being set
for f being FinSequence of D
for g being XFinSequence of D holds f ^ g = f ^ (XFS2FS g)
proof end;

theorem XFF: :: RVSUM_4:42
for D being set
for f being XFinSequence of D
for g being FinSequence of D holds f ^ g = f ^ (FS2XFS g)
proof end;

theorem SFF: :: RVSUM_4:43
for D being set
for f, g being FinSequence of D holds FS2XFS (f ^ g) = (FS2XFS f) ^ (FS2XFS g)
proof end;

definition
let D be set ;
let f be FinSequence of D;
let g be XFinSequence of D;
:: original: ^
redefine func f ^ g -> FinSequence of D;
coherence
f ^ g is FinSequence of D
proof end;
end;

theorem :: RVSUM_4:44
for D being set
for f being FinSequence of D
for g being XFinSequence of D holds FS2XFS (f ^ g) = (FS2XFS f) ^ g
proof end;

theorem SXX: :: RVSUM_4:45
for D being set
for f, g being XFinSequence of D holds XFS2FS (f ^ g) = (XFS2FS f) ^ (XFS2FS g)
proof end;

definition
let D be set ;
let f be XFinSequence of D;
let g be FinSequence of D;
:: original: ^
redefine func f ^ g -> XFinSequence of D;
coherence
f ^ g is XFinSequence of D
proof end;
end;

theorem SSX: :: RVSUM_4:46
for D being set
for f being XFinSequence of D
for g being FinSequence of D holds XFS2FS (f ^ g) = (XFS2FS f) ^ g
proof end;

theorem :: RVSUM_4:47
for D being set
for f, g being XFinSequence of D
for h being FinSequence of D holds
( (f ^ g) ^ h = f ^ (g ^ h) & (f ^ h) ^ g = f ^ (h ^ g) & (h ^ f) ^ g = h ^ (f ^ g) )
proof end;

:: Sums
theorem :: RVSUM_4:48
for f being complex-valued XFinSequence holds Sum (f | 1) = f . 0
proof end;

registration
let n, m be Nat;
let f be n + m -element XFinSequence;
cluster f | n -> n -element ;
coherence
f | n is n -element
proof end;
end;

registration
let n be Nat;
let p be n -element complex-valued XFinSequence;
cluster - p -> n -element ;
coherence
- p is n -element
proof end;
cluster p " -> n -element ;
coherence
p " is n -element
proof end;
cluster p ^2 -> n -element ;
coherence
p ^2 is n -element
proof end;
cluster |.p.| -> n -element ;
coherence
abs p is n -element
proof end;
cluster Rev p -> n -element ;
coherence
Rev p is n -element
proof end;
let m be Nat;
let q be n + m -element complex-valued XFinSequence;
reduce (dom p) /\ (dom q) to dom p;
reducibility
(dom p) /\ (dom q) = dom p
proof end;
cluster p + q -> n -element ;
coherence
p + q is n -element
proof end;
cluster p - q -> n -element ;
coherence
p - q is n -element ;
cluster p (#) q -> n -element ;
coherence
p (#) q is n -element
proof end;
cluster p /" q -> n -element ;
coherence
p /" q is n -element ;
end;

registration
let n be Nat;
let p, q be n -element complex-valued XFinSequence;
cluster p + q -> n -element ;
coherence
p + q is n -element
proof end;
cluster p - q -> n -element ;
coherence
p - q is n -element ;
cluster p (#) q -> n -element ;
coherence
p (#) q is n -element
proof end;
cluster p /" q -> n -element ;
coherence
p /" q is n -element ;
end;

theorem SPP: :: RVSUM_4:49
for n being Nat
for f1, f2 being b1 -element complex-valued XFinSequence holds Sum (f1 + f2) = (Sum f1) + (Sum f2)
proof end;

theorem XCF: :: RVSUM_4:50
for c being Complex holds XFS2FS <%c%> = <*c*>
proof end;

definition
let f be XFinSequence;
func XProduct f -> Element of COMPLEX equals :: RVSUM_4:def 14
multcomplex "**" f;
correctness
coherence
multcomplex "**" f is Element of COMPLEX ;
;
end;

:: deftheorem defines XProduct RVSUM_4:def 14 :
for f being XFinSequence holds XProduct f = multcomplex "**" f;

theorem PFO: :: RVSUM_4:51
for f being empty XFinSequence holds XProduct f = 1
proof end;

registration
let c be Complex;
reduce XProduct <%c%> to c;
reducibility
XProduct <%c%> = c
proof end;
end;

theorem A265: :: RVSUM_4:52
for n being Nat
for f being complex-valued XFinSequence st n in dom f holds
(XProduct (f | n)) * (f . n) = XProduct (f | (n + 1))
proof end;

theorem C265: :: RVSUM_4:53
for n being Nat
for f being Complex_Sequence holds (XProduct (f | n)) * (f . n) = XProduct (f | (n + 1))
proof end;

theorem :: RVSUM_4:54
for f being non empty complex-valued XFinSequence holds XProduct (f | 1) = f . 0
proof end;

theorem :: RVSUM_4:55
for n being Nat
for f1, f2 being b1 -element complex-valued XFinSequence holds XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2)
proof end;

theorem :: RVSUM_4:56
for f being Complex_Sequence
for n being Nat holds XProduct (f | (n + 1)) = (Partial_Product f) . n
proof end;

theorem XPF: :: RVSUM_4:57
for f being complex-valued XFinSequence holds Product (XFS2FS f) = XProduct f
proof end;

theorem :: RVSUM_4:58
for f being FinSequence of COMPLEX holds XProduct (FS2XFS f) = Product f
proof end;

theorem :: RVSUM_4:59
for f being XFinSequence of COMPLEX
for g being FinSequence of COMPLEX holds
( XProduct (f ^ g) = (XProduct f) * (Product g) & Product (g ^ f) = (Product g) * (XProduct f) )
proof end;

theorem XSF: :: RVSUM_4:60
for f being XFinSequence of REAL holds Sum (XFS2FS f) = Sum f
proof end;

theorem RSI: :: RVSUM_4:61
for f being complex-valued XFinSequence holds Sum f = (Sum (Re f)) + (<i> * (Sum (Im f)))
proof end;

theorem RSH: :: RVSUM_4:62
for f being complex-valued Sequence
for n being Nat holds
( Re (Shift (f,n)) = Shift ((Re f),n) & Im (Shift (f,n)) = Shift ((Im f),n) )
proof end;

theorem :: RVSUM_4:63
for f being complex-valued XFinSequence holds
( XFS2FS (Re f) = Re (XFS2FS f) & XFS2FS (Im f) = Im (XFS2FS f) ) by RSH;

theorem XSS: :: RVSUM_4:64
for f being complex-valued XFinSequence holds Sum (XFS2FS f) = Sum f
proof end;

theorem FSS: :: RVSUM_4:65
for f being FinSequence of COMPLEX holds Sum (FS2XFS f) = Sum f
proof end;

theorem SSF: :: RVSUM_4:66
for f being real-valued XFinSequence holds Sum f = Sum (Sequel f)
proof end;

registration
cluster Relation-like omega -defined COMPLEX -valued non empty Sequence-like Function-like V32( omega ) V33( omega , COMPLEX ) complex-valued ext-real-valued real-valued summable for Element of K16(K17(omega,COMPLEX));
existence
ex b1 being real-valued Complex_Sequence st b1 is summable
proof end;
end;

definition
let f be summable Complex_Sequence;
:: original: Re
redefine func Re f -> real-valued summable Complex_Sequence;
coherence
Re f is real-valued summable Complex_Sequence
proof end;
:: original: Im
redefine func Im f -> real-valued summable Complex_Sequence;
coherence
Im f is real-valued summable Complex_Sequence
proof end;
end;

theorem :: RVSUM_4:67
for f being complex-valued XFinSequence holds Sum f = Sum (Sequel f)
proof end;

theorem :: RVSUM_4:68
for f being XFinSequence of COMPLEX
for g being FinSequence of COMPLEX holds
( Sum (f ^ g) = (Sum f) + (Sum g) & Sum (g ^ f) = (Sum g) + (Sum f) )
proof end;