:: 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;

coherence

a -' (a + b) is zero

(a + b) -' a = b

end;
let b be non negative Real;

coherence

a -' (a + b) is zero

proof end;

reducibility (a + b) -' a = b

proof end;

registration

let n, m be Nat;

correctness

compatibility

min (m,n) = n /\ m;

compatibility

n /\ m = min (m,n);

;

correctness

compatibility

n \/ m = max (m,n);

end;
correctness

compatibility

min (m,n) = n /\ m;

proof end;

correctness compatibility

n /\ m = min (m,n);

;

correctness

compatibility

n \/ m = max (m,n);

proof end;

registration

let n, m be non negative Real;

reducibility

min ((n + m),n) = n

max ((n + m),n) = n + m

end;
reducibility

min ((n + m),n) = n

proof end;

reducibility max ((n + m),n) = n + m

proof end;

registration

let D be non empty set ;

let x be sequence of D;

let n be Nat;

reducibility

dom (x | n) = n

( x | n is finite & x | n is Sequence-like ) ;

coherence

x | n is n -element

end;
let x be sequence of D;

let n be Nat;

reducibility

dom (x | n) = n

proof end;

coherence ( x | n is finite & x | n is Sequence-like ) ;

coherence

x | n is n -element

proof end;

registration

let D be non empty set ;

let f, g be sequence of D;

coherence

f +* g is Sequence-like by FUNCT_2:def 1;

end;
let f, g be sequence of D;

coherence

f +* g is Sequence-like by FUNCT_2:def 1;

registration

ex b_{1} being Complex_Sequence st b_{1} is empty-yielding

ex b_{1} being Real_Sequence st b_{1} is empty-yielding

for b_{1} being Complex_Sequence st b_{1} is empty-yielding holds

b_{1} is natural-valued

ex b_{1} being Complex_Sequence st

( b_{1} is constant & b_{1} is real-valued )
end;

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 b

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 b

proof end;

cluster empty-yielding Function-like V33( omega , COMPLEX ) -> natural-valued for Element of K16(K17(omega,COMPLEX));

coherence for b

b

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 b

( b

proof 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;

for n being Nat holds (Partial_Sums s) . n = Sum (s | (Segm (n + 1))) by AFINSQ_2:56;

registration
end;

registration
end;

registration
end;

LmFNK: for n being Nat

for f being b

proof end;

theorem FNK: :: RVSUM_4:8

for n being Nat

for m being non zero Nat

for f being b_{1} + b_{2} -element FinSequence holds f | (n + 1) = (f | n) ^ <*(f . (n + 1))*>

for m being non zero Nat

for f being b

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))

for n being Nat holds Product f = (Product (f | n)) * (Product (f /^ n))

proof end;

:: FINSOP_1 -- +*

definition

let s be Complex_Sequence;

ex b_{1} being Complex_Sequence st

( b_{1} . 0 = s . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * (s . (n + 1)) ) )

for b_{1}, b_{2} being Complex_Sequence st b_{1} . 0 = s . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * (s . (n + 1)) ) & b_{2} . 0 = s . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) * (s . (n + 1)) ) holds

b_{1} = b_{2}

end;
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 ( it . 0 = s . 0 & ( for n being Nat holds it . (n + 1) = (it . n) * (s . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem PP defines Partial_Product RVSUM_4:def 2 :

for s, b_{2} being Complex_Sequence holds

( b_{2} = Partial_Product s iff ( b_{2} . 0 = s . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) * (s . (n + 1)) ) ) );

for s, b

( b

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

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;

compatibility

for b_{1} being set holds

( b_{1} = c |^ n iff b_{1} = (Partial_Product (seq_const c)) . (n - 1) )

end;
let n be non zero Nat;

compatibility

for b

( b

proof 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);

for c being Complex

for n being non zero Nat holds c |^ n = (Partial_Product (seq_const c)) . (n - 1);

registration

for b_{1} being Complex_Sequence st b_{1} is empty-yielding holds

b_{1} is absolutely_summable

for b_{1} being Real_Sequence st b_{1} is empty-yielding holds

b_{1} is absolutely_summable
end;

cluster empty-yielding Function-like V33( omega , COMPLEX ) -> absolutely_summable for Element of K16(K17(omega,COMPLEX));

coherence for b

b

proof end;

cluster empty-yielding Function-like V33( omega , REAL ) -> absolutely_summable for Element of K16(K17(omega,REAL));

coherence for b

b

proof end;

registration

reducibility

Partial_Sums (NAT --> 0) = NAT --> 0

Partial_Product (seq_const 0) = seq_const 0 by COMSEQ324, PARTFUN1:def 2;

for b_{1} being Complex_Sequence holds b_{1} is Sequence-like
by COMSEQ_1:1;

ex b_{1} being sequence of COMPLEX st b_{1} is summable

end;
Partial_Sums (NAT --> 0) = NAT --> 0

proof end;

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 b

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 b

proof end;

registration
end;

registration

let n be Nat;

ex b_{1} being natural-valued XFinSequence st b_{1} is n -element

coherence

n --> k is n -element

end;
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 b

proof end;

let k be object ;coherence

n --> k is n -element

proof end;

registration

let n be Nat;

existence

ex b_{1} being XFinSequence st b_{1} is n -element

reducibility

f | n = f

end;
existence

ex b

proof end;

let f be n -element XFinSequence;reducibility

f | n = f

proof end;

registration
end;

registration
end;

registration
end;

:: Segm

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) )

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;

correctness

coherence

f \/ (Shift (seq,(len f))) is Complex_Sequence;

end;
let seq be Complex_Sequence;

correctness

coherence

f \/ (Shift (seq,(len f))) is Complex_Sequence;

proof 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)));

for f being complex-valued XFinSequence

for seq being Complex_Sequence holds f ^ seq = f \/ (Shift (seq,(len f)));

definition
end;

:: deftheorem defines ^ RVSUM_4:def 5 :

for seq being Complex_Sequence

for f being Function holds seq ^ f = seq;

for seq being Complex_Sequence

for f being Function holds seq ^ f = seq;

theorem :: RVSUM_4:17

for rseq being Real_Sequence

for cseq being Complex_Sequence st cseq = rseq holds

Partial_Product rseq = Partial_Product cseq

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;

correctness

coherence

f \/ (Shift (seq,(len f))) is Complex_Sequence;

end;
let seq be Real_Sequence;

correctness

coherence

f \/ (Shift (seq,(len f))) is Complex_Sequence;

proof 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)));

for f being complex-valued XFinSequence

for seq being Real_Sequence holds f ^ seq = f \/ (Shift (seq,(len f)));

theorem :: RVSUM_4:18

:: may be used for conversion of Real_Sequences into Complex_Sequences

definition

let f be Real_Sequence;

let g be Function;

correctness

coherence

f is real-valued sequence of COMPLEX;

by RSC;

end;
let g be Function;

correctness

coherence

f is real-valued sequence of COMPLEX;

by RSC;

:: deftheorem defines ^ RVSUM_4:def 7 :

for f being Real_Sequence

for g being Function holds f ^ g = f;

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;

reducibility

(f ^ seq) | (dom f) = f

end;
let seq be Complex_Sequence;

reducibility

(f ^ seq) | (dom f) = f

proof end;

registration

let f be complex-valued XFinSequence;

let seq be Real_Sequence;

reducibility

(f ^ seq) | (dom f) = f

end;
let seq be Real_Sequence;

reducibility

(f ^ seq) | (dom f) = f

proof end;

registration

let f be real-valued Complex_Sequence;

coherence

Im f is empty-yielding

Re f = f

end;
coherence

Im f is empty-yielding

proof end;

reducibility Re f = f

proof end;

registration

ex b_{1} being Real_Sequence st b_{1} is empty-yielding

for b_{1} being Real_Sequence holds b_{1} is Sequence-like
by SEQ_1:1;

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 b

proof end;

coherence for b

registration

let r be Real;

coherence

Re (r * <i>) is zero by COMPLEX1:10;

reducibility

Im (r * <i>) = r by COMPLEX1:11;

end;
coherence

Re (r * <i>) is zero by COMPLEX1:10;

reducibility

Im (r * <i>) = r by COMPLEX1:11;

registration

let f be complex-valued XFinSequence;

coherence

( Re f is real-valued & Re f is finite & Re f is Sequence-like )

( Im f is real-valued & Im f is finite & Im f is Sequence-like )

Re f is len f -element

Im f is len f -element

end;
coherence

( Re f is real-valued & Re f is finite & Re f is Sequence-like )

proof end;

coherence ( Im f is real-valued & Im f is finite & Im f is Sequence-like )

proof end;

coherence Re f is len f -element

proof end;

coherence Im f is len f -element

proof end;

registration

let f be complex-valued FinSequence;

coherence

( Re f is real-valued & Re f is FinSequence-like )

( Im f is real-valued & Im f is FinSequence-like )

end;
coherence

( Re f is real-valued & Re f is FinSequence-like )

proof end;

coherence ( Im f is real-valued & Im f is FinSequence-like )

proof end;

registration

let f be complex-valued Function;

reducibility

Re (Re f) = Re f

Re (Im f) = Im f

Im (Re f) is empty-yielding

Im (Im f) is empty-yielding

Re ((Re f) + (<i> (#) (Im f))) = Re f

Im ((Re f) + (<i> (#) (Im f))) = Im f

(Re f) + (<i> (#) (Im f)) = f

end;
reducibility

Re (Re f) = Re f

proof end;

reducibility Re (Im f) = Im f

proof end;

coherence Im (Re f) is empty-yielding

proof end;

coherence Im (Im f) is empty-yielding

proof end;

reducibility Re ((Re f) + (<i> (#) (Im f))) = Re f

proof end;

reducibility Im ((Re f) + (<i> (#) (Im f))) = Im f

proof end;

reducibility (Re f) + (<i> (#) (Im f)) = f

proof end;

registration
end;

registration

let f be finite complex-valued Sequence;

let n be Nat;

coherence

Shift (f,n) is finite ;

coherence

Shift (f,n) is len f -element

end;
let n be Nat;

coherence

Shift (f,n) is finite ;

coherence

Shift (f,n) is len f -element

proof end;

definition
end;

:: deftheorem defines Sequel RVSUM_4:def 8 :

for f being complex-valued XFinSequence holds Sequel f = (NAT --> 0) +* f;

for f being complex-valued XFinSequence holds Sequel f = (NAT --> 0) +* f;

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

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

for x being Nat st ( for k being Nat st k >= x holds

seq . k = 0 ) holds

seq is summable

proof end;

:: Concatenation of (X)FinSequences

definition

let f be XFinSequence;

let g be FinSequence;

ex b_{1} being XFinSequence st

( dom b_{1} = (len f) + (len g) & ( for k being Nat st k in dom f holds

b_{1} . k = f . k ) & ( for k being Nat st k in dom g holds

b_{1} . (((len f) + k) - 1) = g . k ) )

for b_{1}, b_{2} being XFinSequence st dom b_{1} = (len f) + (len g) & ( for k being Nat st k in dom f holds

b_{1} . k = f . k ) & ( for k being Nat st k in dom g holds

b_{1} . (((len f) + k) - 1) = g . k ) & dom b_{2} = (len f) + (len g) & ( for k being Nat st k in dom f holds

b_{2} . k = f . k ) & ( for k being Nat st k in dom g holds

b_{2} . (((len f) + k) - 1) = g . k ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( dom b

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

:: deftheorem Def1 defines ^ RVSUM_4:def 9 :

for f being XFinSequence

for g being FinSequence

for b_{3} being XFinSequence holds

( b_{3} = f ^ g iff ( dom b_{3} = (len f) + (len g) & ( for k being Nat st k in dom f holds

b_{3} . k = f . k ) & ( for k being Nat st k in dom g holds

b_{3} . (((len f) + k) - 1) = g . k ) ) );

for f being XFinSequence

for g being FinSequence

for b

( b

b

b

definition

let f be FinSequence;

let g be XFinSequence;

ex b_{1} being FinSequence st

( dom b_{1} = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds

b_{1} . k = f . k ) & ( for k being Nat st k in dom g holds

b_{1} . (((len f) + k) + 1) = g . k ) )

for b_{1}, b_{2} being FinSequence st dom b_{1} = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds

b_{1} . k = f . k ) & ( for k being Nat st k in dom g holds

b_{1} . (((len f) + k) + 1) = g . k ) & dom b_{2} = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds

b_{2} . k = f . k ) & ( for k being Nat st k in dom g holds

b_{2} . (((len f) + k) + 1) = g . k ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( dom b

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

:: deftheorem Def2 defines ^ RVSUM_4:def 10 :

for f being FinSequence

for g being XFinSequence

for b_{3} being FinSequence holds

( b_{3} = f ^ g iff ( dom b_{3} = Seg ((len f) + (len g)) & ( for k being Nat st k in dom f holds

b_{3} . k = f . k ) & ( for k being Nat st k in dom g holds

b_{3} . (((len f) + k) + 1) = g . k ) ) );

for f being FinSequence

for g being XFinSequence

for b

( b

b

b

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) )

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;

coherence

f ^ g is n + m -element

g ^ f is n + m -element

end;
let f be n -element XFinSequence;

let g be m -element FinSequence;

coherence

f ^ g is n + m -element

proof end;

coherence g ^ f is n + m -element

proof 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 ) )

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 ) )

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) )

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))

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))

for g being XFinSequence holds dom (f \/ (Shift (g,((len f) + 1)))) = Seg ((len f) + (len g))

proof end;

registration
end;

registration
end;

registration

let f be XFinSequence;

let g be FinSequence;

reducibility

(f ^ g) | (len f) = f

(g ^ f) | (len g) = g

end;
let g be FinSequence;

reducibility

(f ^ g) | (len f) = f

proof end;

reducibility (g ^ f) | (len g) = g

proof 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

for f being XFinSequence

for g being FinSequence of D holds (f ^ g) /^ (len f) = FS2XFS g

proof end;

theorem :: RVSUM_4:36

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

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;

coherence

XFS2FS f is FinSequence of D

for b_{1} being FinSequence of D holds

( b_{1} = XFS2FS f iff b_{1} = (<*> D) ^ f )

end;
let f be XFinSequence of D;

coherence

XFS2FS f is FinSequence of D

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines XFS2FS RVSUM_4:def 11 :

for D being set

for f being XFinSequence of D holds XFS2FS f = (<*> D) ^ f;

for D being set

for f being XFinSequence of D holds XFS2FS f = (<*> D) ^ f;

definition

let D be set ;

let f be XFinSequence of D;

coherence

XFS2FS f is FinSequence of D

for b_{1} being FinSequence of D holds

( b_{1} = XFS2FS f iff b_{1} = Shift (f,1) )

end;
let f be XFinSequence of D;

coherence

XFS2FS f is FinSequence of D

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines XFS2FS RVSUM_4:def 12 :

for D being set

for f being XFinSequence of D holds XFS2FS f = Shift (f,1);

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;

compatibility

for b_{1} being set holds

( b_{1} = FS2XFS f iff b_{1} = (<%> D) ^ f )

end;
let f be FinSequence of D;

compatibility

for b

( b

proof end;

:: deftheorem defines FS2XFS RVSUM_4:def 13 :

for D being set

for f being FinSequence of D holds FS2XFS f = (<%> D) ^ f;

for D being set

for f being FinSequence of D holds FS2XFS f = (<%> D) ^ f;

registration

let f be XFinSequence of REAL ;

reducibility

(Sequel f) | (dom f) = f ;

coherence

Shift (f,1) is FinSequence-like

(Sequel f) ^\ (dom f) is empty-yielding

end;
reducibility

(Sequel f) | (dom f) = f ;

coherence

Shift (f,1) is FinSequence-like

proof end;

coherence (Sequel f) ^\ (dom f) is empty-yielding

proof 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)

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)

for f being XFinSequence of D

for g being FinSequence of D holds f ^ g = 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

end;
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;

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

for f being FinSequence of D

for g being XFinSequence of D holds FS2XFS (f ^ g) = (FS2XFS f) ^ 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

end;
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;

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

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) )

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

registration
end;

registration

let n be Nat;

let p be n -element complex-valued XFinSequence;

coherence

- p is n -element

p " is n -element

p ^2 is n -element

abs p is n -element

Rev p is n -element

let q be n + m -element complex-valued XFinSequence;

reducibility

(dom p) /\ (dom q) = dom p

p + q is n -element

p - q is n -element ;

coherence

p (#) q is n -element

p /" q is n -element ;

end;
let p be n -element complex-valued XFinSequence;

coherence

- p is n -element

proof end;

coherence p " is n -element

proof end;

coherence p ^2 is n -element

proof end;

coherence abs p is n -element

proof end;

coherence Rev p is n -element

proof end;

let m be Nat;let q be n + m -element complex-valued XFinSequence;

reducibility

(dom p) /\ (dom q) = dom p

proof end;

coherence p + q is n -element

proof end;

coherence p - q is n -element ;

coherence

p (#) q is n -element

proof end;

coherence p /" q is n -element ;

registration

let n be Nat;

let p, q be n -element complex-valued XFinSequence;

coherence

p + q is n -element

p - q is n -element ;

coherence

p (#) q is n -element

p /" q is n -element ;

end;
let p, q be n -element complex-valued XFinSequence;

coherence

p + q is n -element

proof end;

coherence p - q is n -element ;

coherence

p (#) q is n -element

proof end;

coherence p /" q is n -element ;

theorem SPP: :: RVSUM_4:49

for n being Nat

for f1, f2 being b_{1} -element complex-valued XFinSequence holds Sum (f1 + f2) = (Sum f1) + (Sum f2)

for f1, f2 being b

proof end;

definition
end;

:: deftheorem defines XProduct RVSUM_4:def 14 :

for f being XFinSequence holds XProduct f = multcomplex "**" f;

for f being XFinSequence holds XProduct f = multcomplex "**" f;

registration
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))

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))

for f being Complex_Sequence holds (XProduct (f | n)) * (f . n) = XProduct (f | (n + 1))

proof end;

theorem :: RVSUM_4:55

for n being Nat

for f1, f2 being b_{1} -element complex-valued XFinSequence holds XProduct (f1 (#) f2) = (XProduct f1) * (XProduct f2)

for f1, f2 being b

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) )

for g being FinSequence of COMPLEX holds

( XProduct (f ^ g) = (XProduct f) * (Product g) & Product (g ^ f) = (Product g) * (XProduct 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) )

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

registration

ex b_{1} being real-valued Complex_Sequence st b_{1} is summable
end;

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 b

proof 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

redefine func Im f -> real-valued summable Complex_Sequence;

coherence

Im f is real-valued summable Complex_Sequence

end;
:: original: Re

redefine func Re f -> real-valued summable Complex_Sequence;

coherence

Re f is real-valued summable Complex_Sequence

proof end;

:: original: Imredefine func Im f -> real-valued summable Complex_Sequence;

coherence

Im f is real-valued summable Complex_Sequence

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) )

for g being FinSequence of COMPLEX holds

( Sum (f ^ g) = (Sum f) + (Sum g) & Sum (g ^ f) = (Sum g) + (Sum f) )

proof end;