:: by Agnieszka Banachowicz and Anna Winnicka

::

:: Received November 5, 1993

:: Copyright (c) 1993-2018 Association of Mizar Users

theorem Th1: :: COMSEQ_1:1

for f being Function holds

( f is Complex_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds

f . x is Element of COMPLEX ) ) )

( f is Complex_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds

f . x is Element of COMPLEX ) ) )

proof end;

theorem Th2: :: COMSEQ_1:2

for f being Function holds

( f is Complex_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) )

( f is Complex_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) )

proof end;

registration

ex b_{1} being Complex_Sequence st b_{1} is non-zero
end;

cluster Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) non-zero V44() for Complex_Sequence;

existence ex b

proof end;

theorem Th3: :: COMSEQ_1:3

for seq being Complex_Sequence holds

( seq is non-zero iff for x being set st x in NAT holds

seq . x <> 0c )

( seq is non-zero iff for x being set st x in NAT holds

seq . x <> 0c )

proof end;

theorem Th4: :: COMSEQ_1:4

for seq being Complex_Sequence holds

( seq is non-zero iff for n being Element of NAT holds seq . n <> 0c )

( seq is non-zero iff for n being Element of NAT holds seq . n <> 0c )

proof end;

theorem :: COMSEQ_1:5

for IT being non-zero Complex_Sequence holds rng IT c= COMPLEX \ {0c} by ORDINAL1:def 15, ZFMISC_1:34;

theorem Th8: :: COMSEQ_1:8

for seq1, seq2, seq3 being Complex_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)

proof end;

theorem Th9: :: COMSEQ_1:9

for seq1, seq2, seq3 being Complex_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)

proof end;

theorem :: COMSEQ_1:10

theorem Th12: :: COMSEQ_1:12

for r being Complex

for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2

for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2

proof end;

theorem Th13: :: COMSEQ_1:13

for r being Complex

for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)

for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)

proof end;

theorem Th14: :: COMSEQ_1:14

for seq1, seq2, seq3 being Complex_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)

proof end;

theorem :: COMSEQ_1:15

theorem Th16: :: COMSEQ_1:16

for r being Complex

for seq1, seq2 being Complex_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)

for seq1, seq2 being Complex_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)

proof end;

theorem Th18: :: COMSEQ_1:18

for r being Complex

for seq1, seq2 being Complex_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)

for seq1, seq2 being Complex_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)

proof end;

theorem :: COMSEQ_1:19

for r being Complex

for seq, seq1 being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq

for seq, seq1 being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq

proof end;

theorem :: COMSEQ_1:26

::$CT

theorem Th28: :: COMSEQ_1:29

for seq, seq1 being Complex_Sequence holds

( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )

( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )

proof end;

theorem :: COMSEQ_1:32

for seq, seq1, seq9, seq19 being Complex_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)

proof end;

theorem :: COMSEQ_1:33

for seq, seq1 being Complex_Sequence st seq is non-zero & seq1 is non-zero holds

seq /" seq1 is non-zero

seq /" seq1 is non-zero

proof end;

theorem Th36: :: COMSEQ_1:37

for seq, seq1, seq2 being Complex_Sequence st seq1 is non-zero holds

seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)

seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)

proof end;

theorem Th37: :: COMSEQ_1:38

for r being Complex

for seq being Complex_Sequence st r <> 0c & seq is non-zero holds

r (#) seq is non-zero

for seq being Complex_Sequence st r <> 0c & seq is non-zero holds

r (#) seq is non-zero

proof end;

theorem :: COMSEQ_1:39

theorem :: COMSEQ_1:42

for seq, seq1 being Complex_Sequence st seq is non-zero holds

( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )

( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )

proof end;

theorem :: COMSEQ_1:43

for seq, seq1, seq19 being Complex_Sequence holds

( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )

( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )

proof end;

theorem :: COMSEQ_1:44

for seq, seq1, seq9, seq19 being Complex_Sequence st seq is non-zero & seq9 is non-zero holds

( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )

( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )

proof end;

theorem :: COMSEQ_1:45

for seq, seq1, seq9, seq19 being Complex_Sequence holds (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)

proof end;

::$CT