:: COMSEQ_1 semantic presentation begin definition mode Complex_Sequence is sequence of COMPLEX; end; 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 ) ) ) proof let f be Function; ::_thesis: ( f is Complex_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of COMPLEX ) ) ) thus ( f is Complex_Sequence implies ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of COMPLEX ) ) ) ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of COMPLEX ) implies f is Complex_Sequence ) proof assume A1: f is Complex_Sequence ; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds f . x is Element of COMPLEX ) ) hence A2: dom f = NAT by FUNCT_2:def_1; ::_thesis: for x being set st x in NAT holds f . x is Element of COMPLEX let x be set ; ::_thesis: ( x in NAT implies f . x is Element of COMPLEX ) assume x in NAT ; ::_thesis: f . x is Element of COMPLEX then A3: f . x in rng f by A2, FUNCT_1:def_3; rng f c= COMPLEX by A1, RELAT_1:def_19; hence f . x is Element of COMPLEX by A3; ::_thesis: verum end; assume that A4: dom f = NAT and A5: for x being set st x in NAT holds f . x is Element of COMPLEX ; ::_thesis: f is Complex_Sequence now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_COMPLEX let y be set ; ::_thesis: ( y in rng f implies y in COMPLEX ) assume y in rng f ; ::_thesis: y in COMPLEX then consider x being set such that A6: x in dom f and A7: y = f . x by FUNCT_1:def_3; f . x is Element of COMPLEX by A4, A5, A6; hence y in COMPLEX by A7; ::_thesis: verum end; then rng f c= COMPLEX by TARSKI:def_3; hence f is Complex_Sequence by A4, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum 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 ) ) ) proof let f be Function; ::_thesis: ( f is Complex_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) ) thus ( f is Complex_Sequence implies ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) ) by Th1; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) implies f is Complex_Sequence ) assume that A1: dom f = NAT and A2: for n being Element of NAT holds f . n is Element of COMPLEX ; ::_thesis: f is Complex_Sequence for x being set st x in NAT holds f . x is Element of COMPLEX by A2; hence f is Complex_Sequence by A1, Th1; ::_thesis: verum end; scheme :: COMSEQ_1:sch 1 ExComplexSeq{ F1( set ) -> complex number } : ex seq being Complex_Sequence st for n being Element of NAT holds seq . n = F1(n) proof defpred S1[ set , set ] means ex n being Element of NAT st ( n = \$1 & \$2 = F1(n) ); A1: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ ex_y_being_set_st_S1[x,y] let x be set ; ::_thesis: ( x in NAT implies ex y being set st S1[x,y] ) assume x in NAT ; ::_thesis: ex y being set st S1[x,y] then consider n being Element of NAT such that A2: n = x ; reconsider r2 = F1(n) as set ; take y = r2; ::_thesis: S1[x,y] thus S1[x,y] by A2; ::_thesis: verum end; consider f being Function such that A3: dom f = NAT and A4: for x being set st x in NAT holds S1[x,f . x] from CLASSES1:sch_1(A1); now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ f_._x_is_Element_of_COMPLEX let x be set ; ::_thesis: ( x in NAT implies f . x is Element of COMPLEX ) assume x in NAT ; ::_thesis: f . x is Element of COMPLEX then ex n being Element of NAT st ( n = x & f . x = F1(n) ) by A4; hence f . x is Element of COMPLEX by XCMPLX_0:def_2; ::_thesis: verum end; then reconsider f = f as Complex_Sequence by A3, Th1; take seq = f; ::_thesis: for n being Element of NAT holds seq . n = F1(n) let n be Element of NAT ; ::_thesis: seq . n = F1(n) ex k being Element of NAT st ( k = n & seq . n = F1(k) ) by A4; hence seq . n = F1(n) ; ::_thesis: verum end; notation let f be complex-valued Relation; synonym non-zero f for non-empty ; end; registration cluster Relation-like non-zero NAT -defined COMPLEX -valued Function-like non zero V14( NAT ) V18( NAT , COMPLEX ) complex-valued for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is non-zero proof take s = NAT --> 1r; ::_thesis: s is non-zero rng s = {1} by FUNCOP_1:8; hence not 0 in rng s by TARSKI:def_1; :: according to RELAT_1:def_9 ::_thesis: verum end; 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 ) proof let seq be Complex_Sequence; ::_thesis: ( seq is non-zero iff for x being set st x in NAT holds seq . x <> 0c ) thus ( seq is non-zero implies for x being set st x in NAT holds seq . x <> 0c ) ::_thesis: ( ( for x being set st x in NAT holds seq . x <> 0c ) implies seq is non-zero ) proof assume A1: seq is non-zero ; ::_thesis: for x being set st x in NAT holds seq . x <> 0c let x be set ; ::_thesis: ( x in NAT implies seq . x <> 0c ) assume x in NAT ; ::_thesis: seq . x <> 0c then x in dom seq by Th2; then seq . x in rng seq by FUNCT_1:def_3; hence seq . x <> 0c by A1, RELAT_1:def_9; ::_thesis: verum end; assume A2: for x being set st x in NAT holds seq . x <> 0c ; ::_thesis: seq is non-zero assume 0 in rng seq ; :: according to RELAT_1:def_9 ::_thesis: contradiction then ex x being set st ( x in dom seq & seq . x = 0 ) by FUNCT_1:def_3; hence contradiction by A2; ::_thesis: verum 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 ) proof let seq be Complex_Sequence; ::_thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0c ) thus ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0c ) by Th3; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0c ) implies seq is non-zero ) assume for n being Element of NAT holds seq . n <> 0c ; ::_thesis: seq is non-zero then for x being set st x in NAT holds seq . x <> 0c ; hence seq is non-zero by Th3; ::_thesis: verum end; theorem :: COMSEQ_1:5 for IT being non-zero Complex_Sequence holds rng IT c= COMPLEX \ {0c} proof let IT be non-zero Complex_Sequence; ::_thesis: rng IT c= COMPLEX \ {0c} not 0c in rng IT by RELAT_1:def_9; hence rng IT c= COMPLEX \ {0c} by ZFMISC_1:34; ::_thesis: verum end; theorem :: COMSEQ_1:6 for r being Element of COMPLEX ex seq being Complex_Sequence st rng seq = {r} proof let r be Element of COMPLEX ; ::_thesis: ex seq being Complex_Sequence st rng seq = {r} consider f being Function such that A1: dom f = NAT and A2: rng f = {r} by FUNCT_1:5; now__::_thesis:_for_x_being_set_st_x_in_{r}_holds_ x_in_COMPLEX let x be set ; ::_thesis: ( x in {r} implies x in COMPLEX ) assume x in {r} ; ::_thesis: x in COMPLEX then x = r by TARSKI:def_1; hence x in COMPLEX ; ::_thesis: verum end; then rng f c= COMPLEX by A2, TARSKI:def_3; then reconsider f = f as Complex_Sequence by A1, FUNCT_2:def_1, RELSET_1:4; take f ; ::_thesis: rng f = {r} thus rng f = {r} by A2; ::_thesis: verum end; theorem Th7: :: COMSEQ_1:7 for seq1, seq2, seq3 being Complex_Sequence holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) proof let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_+_seq3)_._n_=_(seq1_+_(seq2_+_seq3))_._n let n be Element of NAT ; ::_thesis: ((seq1 + seq2) + seq3) . n = (seq1 + (seq2 + seq3)) . n thus ((seq1 + seq2) + seq3) . n = ((seq1 + seq2) . n) + (seq3 . n) by VALUED_1:1 .= ((seq1 . n) + (seq2 . n)) + (seq3 . n) by VALUED_1:1 .= (seq1 . n) + ((seq2 . n) + (seq3 . n)) .= (seq1 . n) + ((seq2 + seq3) . n) by VALUED_1:1 .= (seq1 + (seq2 + seq3)) . n by VALUED_1:1 ; ::_thesis: verum end; hence (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) by FUNCT_2:63; ::_thesis: verum end; theorem Th8: :: COMSEQ_1:8 for seq1, seq2, seq3 being Complex_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3) proof let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_(#)_seq2)_(#)_seq3)_._n_=_(seq1_(#)_(seq2_(#)_seq3))_._n let n be Element of NAT ; ::_thesis: ((seq1 (#) seq2) (#) seq3) . n = (seq1 (#) (seq2 (#) seq3)) . n thus ((seq1 (#) seq2) (#) seq3) . n = ((seq1 (#) seq2) . n) * (seq3 . n) by VALUED_1:5 .= ((seq1 . n) * (seq2 . n)) * (seq3 . n) by VALUED_1:5 .= (seq1 . n) * ((seq2 . n) * (seq3 . n)) .= (seq1 . n) * ((seq2 (#) seq3) . n) by VALUED_1:5 .= (seq1 (#) (seq2 (#) seq3)) . n by VALUED_1:5 ; ::_thesis: verum end; hence (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3) by FUNCT_2:63; ::_thesis: verum end; theorem Th9: :: COMSEQ_1:9 for seq1, seq2, seq3 being Complex_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3) proof let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_(#)_seq3)_._n_=_((seq1_(#)_seq3)_+_(seq2_(#)_seq3))_._n let n be Element of NAT ; ::_thesis: ((seq1 + seq2) (#) seq3) . n = ((seq1 (#) seq3) + (seq2 (#) seq3)) . n thus ((seq1 + seq2) (#) seq3) . n = ((seq1 + seq2) . n) * (seq3 . n) by VALUED_1:5 .= ((seq1 . n) + (seq2 . n)) * (seq3 . n) by VALUED_1:1 .= ((seq1 . n) * (seq3 . n)) + ((seq2 . n) * (seq3 . n)) .= ((seq1 (#) seq3) . n) + ((seq2 . n) * (seq3 . n)) by VALUED_1:5 .= ((seq1 (#) seq3) . n) + ((seq2 (#) seq3) . n) by VALUED_1:5 .= ((seq1 (#) seq3) + (seq2 (#) seq3)) . n by VALUED_1:1 ; ::_thesis: verum end; hence (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3) by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_1:10 for seq3, seq1, seq2 being Complex_Sequence holds seq3 (#) (seq1 + seq2) = (seq3 (#) seq1) + (seq3 (#) seq2) by Th9; theorem :: COMSEQ_1:11 for seq being Complex_Sequence holds - seq = (- 1r) (#) seq ; theorem Th12: :: COMSEQ_1:12 for r being Element of COMPLEX for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 proof let r be Element of COMPLEX ; ::_thesis: for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 let seq1, seq2 be Complex_Sequence; ::_thesis: r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_(#)_seq2))_._n_=_((r_(#)_seq1)_(#)_seq2)_._n let n be Element of NAT ; ::_thesis: (r (#) (seq1 (#) seq2)) . n = ((r (#) seq1) (#) seq2) . n thus (r (#) (seq1 (#) seq2)) . n = r * ((seq1 (#) seq2) . n) by VALUED_1:6 .= r * ((seq1 . n) * (seq2 . n)) by VALUED_1:5 .= (r * (seq1 . n)) * (seq2 . n) .= ((r (#) seq1) . n) * (seq2 . n) by VALUED_1:6 .= ((r (#) seq1) (#) seq2) . n by VALUED_1:5 ; ::_thesis: verum end; hence r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2 by FUNCT_2:63; ::_thesis: verum end; theorem Th13: :: COMSEQ_1:13 for r being Element of COMPLEX for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) proof let r be Element of COMPLEX ; ::_thesis: for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) let seq1, seq2 be Complex_Sequence; ::_thesis: r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_(#)_seq2))_._n_=_(seq1_(#)_(r_(#)_seq2))_._n let n be Element of NAT ; ::_thesis: (r (#) (seq1 (#) seq2)) . n = (seq1 (#) (r (#) seq2)) . n thus (r (#) (seq1 (#) seq2)) . n = r * ((seq1 (#) seq2) . n) by VALUED_1:6 .= r * ((seq1 . n) * (seq2 . n)) by VALUED_1:5 .= (seq1 . n) * (r * (seq2 . n)) .= (seq1 . n) * ((r (#) seq2) . n) by VALUED_1:6 .= (seq1 (#) (r (#) seq2)) . n by VALUED_1:5 ; ::_thesis: verum end; hence r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) by FUNCT_2:63; ::_thesis: verum end; theorem Th14: :: COMSEQ_1:14 for seq1, seq2, seq3 being Complex_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3) proof let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3) thus (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) + ((- seq2) (#) seq3) by Th9 .= (seq1 (#) seq3) + (((- 1r) (#) seq2) (#) seq3) .= (seq1 (#) seq3) + ((- 1r) (#) (seq2 (#) seq3)) by Th12 .= (seq1 (#) seq3) - (seq2 (#) seq3) ; ::_thesis: verum end; theorem :: COMSEQ_1:15 for seq3, seq1, seq2 being Complex_Sequence holds (seq3 (#) seq1) - (seq3 (#) seq2) = seq3 (#) (seq1 - seq2) by Th14; theorem Th16: :: COMSEQ_1:16 for r being Element of COMPLEX for seq1, seq2 being Complex_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) proof let r be Element of COMPLEX ; ::_thesis: for seq1, seq2 being Complex_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) let seq1, seq2 be Complex_Sequence; ::_thesis: r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(seq1_+_seq2))_._n_=_((r_(#)_seq1)_+_(r_(#)_seq2))_._n let n be Element of NAT ; ::_thesis: (r (#) (seq1 + seq2)) . n = ((r (#) seq1) + (r (#) seq2)) . n thus (r (#) (seq1 + seq2)) . n = r * ((seq1 + seq2) . n) by VALUED_1:6 .= r * ((seq1 . n) + (seq2 . n)) by VALUED_1:1 .= (r * (seq1 . n)) + (r * (seq2 . n)) .= ((r (#) seq1) . n) + (r * (seq2 . n)) by VALUED_1:6 .= ((r (#) seq1) . n) + ((r (#) seq2) . n) by VALUED_1:6 .= ((r (#) seq1) + (r (#) seq2)) . n by VALUED_1:1 ; ::_thesis: verum end; hence r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2) by FUNCT_2:63; ::_thesis: verum end; theorem Th17: :: COMSEQ_1:17 for r, p being Element of COMPLEX for seq being Complex_Sequence holds (r * p) (#) seq = r (#) (p (#) seq) proof let r, p be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence holds (r * p) (#) seq = r (#) (p (#) seq) let seq be Complex_Sequence; ::_thesis: (r * p) (#) seq = r (#) (p (#) seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_*_p)_(#)_seq)_._n_=_(r_(#)_(p_(#)_seq))_._n let n be Element of NAT ; ::_thesis: ((r * p) (#) seq) . n = (r (#) (p (#) seq)) . n thus ((r * p) (#) seq) . n = (r * p) * (seq . n) by VALUED_1:6 .= r * (p * (seq . n)) .= r * ((p (#) seq) . n) by VALUED_1:6 .= (r (#) (p (#) seq)) . n by VALUED_1:6 ; ::_thesis: verum end; hence (r * p) (#) seq = r (#) (p (#) seq) by FUNCT_2:63; ::_thesis: verum end; theorem Th18: :: COMSEQ_1:18 for r being Element of COMPLEX for seq1, seq2 being Complex_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2) proof let r be Element of COMPLEX ; ::_thesis: for seq1, seq2 being Complex_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2) let seq1, seq2 be Complex_Sequence; ::_thesis: r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2) thus r (#) (seq1 - seq2) = (r (#) seq1) + (r (#) (- seq2)) by Th16 .= (r (#) seq1) + (r (#) ((- 1r) (#) seq2)) .= (r (#) seq1) + (((- 1r) * r) (#) seq2) by Th17 .= (r (#) seq1) + ((- 1r) (#) (r (#) seq2)) by Th17 .= (r (#) seq1) - (r (#) seq2) ; ::_thesis: verum end; theorem :: COMSEQ_1:19 for r being Element of COMPLEX for seq1, seq being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq proof let r be Element of COMPLEX ; ::_thesis: for seq1, seq being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq let seq1, seq be Complex_Sequence; ::_thesis: r (#) (seq1 /" seq) = (r (#) seq1) /" seq thus r (#) (seq1 /" seq) = r (#) (seq1 (#) (seq ")) .= (r (#) seq1) /" seq by Th12 ; ::_thesis: verum end; theorem :: COMSEQ_1:20 for seq1, seq2, seq3 being Complex_Sequence holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 proof let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3 thus seq1 - (seq2 + seq3) = seq1 + ((- 1r) (#) (seq2 + seq3)) .= seq1 + (((- 1r) (#) seq2) + ((- 1r) (#) seq3)) by Th16 .= seq1 + ((- seq2) + ((- 1r) (#) seq3)) .= seq1 + ((- seq2) + (- seq3)) .= (seq1 - seq2) - seq3 by Th7 ; ::_thesis: verum end; theorem :: COMSEQ_1:21 for seq being Complex_Sequence holds 1r (#) seq = seq proof let seq be Complex_Sequence; ::_thesis: 1r (#) seq = seq now__::_thesis:_for_n_being_Element_of_NAT_holds_(1r_(#)_seq)_._n_=_seq_._n let n be Element of NAT ; ::_thesis: (1r (#) seq) . n = seq . n thus (1r (#) seq) . n = 1r * (seq . n) by VALUED_1:6 .= seq . n ; ::_thesis: verum end; hence 1r (#) seq = seq by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_1:22 for seq being Complex_Sequence holds - (- seq) = seq ; theorem :: COMSEQ_1:23 for seq1, seq2 being Complex_Sequence holds seq1 - (- seq2) = seq1 + seq2 ; theorem :: COMSEQ_1:24 for seq1, seq2, seq3 being Complex_Sequence holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 proof let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3 thus seq1 - (seq2 - seq3) = seq1 + ((- 1r) (#) (seq2 - seq3)) .= seq1 + (((- 1r) (#) seq2) - ((- 1r) (#) seq3)) by Th18 .= seq1 + ((- seq2) - ((- 1r) (#) seq3)) .= seq1 + ((- seq2) - (- seq3)) .= (seq1 - seq2) + seq3 by Th7 ; ::_thesis: verum end; theorem :: COMSEQ_1:25 for seq1, seq2, seq3 being Complex_Sequence holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 proof let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 thus seq1 + (seq2 - seq3) = seq1 + (seq2 + (- seq3)) .= (seq1 + seq2) - seq3 by Th7 ; ::_thesis: verum end; theorem :: COMSEQ_1:26 for seq1, seq2 being Complex_Sequence holds ( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) ) proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) ) thus (- seq1) (#) seq2 = ((- 1r) (#) seq1) (#) seq2 .= (- 1r) (#) (seq1 (#) seq2) by Th12 .= - (seq1 (#) seq2) ; ::_thesis: seq1 (#) (- seq2) = - (seq1 (#) seq2) thus seq1 (#) (- seq2) = seq1 (#) ((- 1r) (#) seq2) .= (- 1r) (#) (seq1 (#) seq2) by Th13 .= - (seq1 (#) seq2) ; ::_thesis: verum end; theorem Th27: :: COMSEQ_1:27 for seq being Complex_Sequence st seq is non-zero holds seq " is non-zero proof let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies seq " is non-zero ) assume that A1: seq is non-zero and A2: not seq " is non-zero ; ::_thesis: contradiction consider n1 being Element of NAT such that A3: (seq ") . n1 = 0c by A2, Th4; (seq . n1) " = (seq ") . n1 by VALUED_1:10; hence contradiction by A1, A3, Th4, XCMPLX_1:202; ::_thesis: verum end; theorem :: COMSEQ_1:28 canceled; theorem Th29: :: COMSEQ_1:29 for seq, seq1 being Complex_Sequence holds ( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero ) proof let seq, seq1 be Complex_Sequence; ::_thesis: ( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero ) thus ( seq is non-zero & seq1 is non-zero implies seq (#) seq1 is non-zero ) ::_thesis: ( seq (#) seq1 is non-zero implies ( seq is non-zero & seq1 is non-zero ) ) proof assume A1: ( seq is non-zero & seq1 is non-zero ) ; ::_thesis: seq (#) seq1 is non-zero now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_(#)_seq1)_._n_<>_0c let n be Element of NAT ; ::_thesis: (seq (#) seq1) . n <> 0c A2: (seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5; ( seq . n <> 0c & seq1 . n <> 0c ) by A1, Th4; hence (seq (#) seq1) . n <> 0c by A2; ::_thesis: verum end; hence seq (#) seq1 is non-zero by Th4; ::_thesis: verum end; assume A3: seq (#) seq1 is non-zero ; ::_thesis: ( seq is non-zero & seq1 is non-zero ) now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<>_0c let n be Element of NAT ; ::_thesis: seq . n <> 0c (seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5; hence seq . n <> 0c by A3, Th4; ::_thesis: verum end; hence seq is non-zero by Th4; ::_thesis: seq1 is non-zero now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_<>_0c let n be Element of NAT ; ::_thesis: seq1 . n <> 0c (seq (#) seq1) . n = (seq . n) * (seq1 . n) by VALUED_1:5; hence seq1 . n <> 0c by A3, Th4; ::_thesis: verum end; hence seq1 is non-zero by Th4; ::_thesis: verum end; theorem Th30: :: COMSEQ_1:30 for seq, seq1 being Complex_Sequence holds (seq ") (#) (seq1 ") = (seq (#) seq1) " proof let seq, seq1 be Complex_Sequence; ::_thesis: (seq ") (#) (seq1 ") = (seq (#) seq1) " now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_")_(#)_(seq1_"))_._n_=_((seq_(#)_seq1)_")_._n let n be Element of NAT ; ::_thesis: ((seq ") (#) (seq1 ")) . n = ((seq (#) seq1) ") . n thus ((seq ") (#) (seq1 ")) . n = ((seq ") . n) * ((seq1 ") . n) by VALUED_1:5 .= ((seq ") . n) * ((seq1 . n) ") by VALUED_1:10 .= ((seq . n) ") * ((seq1 . n) ") by VALUED_1:10 .= ((seq . n) * (seq1 . n)) " by XCMPLX_1:204 .= ((seq (#) seq1) . n) " by VALUED_1:5 .= ((seq (#) seq1) ") . n by VALUED_1:10 ; ::_thesis: verum end; hence (seq ") (#) (seq1 ") = (seq (#) seq1) " by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_1:31 for seq, seq1 being Complex_Sequence st seq is non-zero holds (seq1 /" seq) (#) seq = seq1 proof let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is non-zero implies (seq1 /" seq) (#) seq = seq1 ) assume A1: seq is non-zero ; ::_thesis: (seq1 /" seq) (#) seq = seq1 now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_/"_seq)_(#)_seq)_._n_=_seq1_._n let n be Element of NAT ; ::_thesis: ((seq1 /" seq) (#) seq) . n = seq1 . n A2: seq . n <> 0c by A1, Th4; thus ((seq1 /" seq) (#) seq) . n = ((seq1 (#) (seq ")) . n) * (seq . n) by VALUED_1:5 .= ((seq1 . n) * ((seq ") . n)) * (seq . n) by VALUED_1:5 .= ((seq1 . n) * ((seq . n) ")) * (seq . n) by VALUED_1:10 .= (seq1 . n) * (((seq . n) ") * (seq . n)) .= (seq1 . n) * 1r by A2, XCMPLX_0:def_7 .= seq1 . n ; ::_thesis: verum end; hence (seq1 /" seq) (#) seq = seq1 by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_1:32 for seq9, seq, seq19, seq1 being Complex_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1) proof let seq9, seq, seq19, seq1 be Complex_Sequence; ::_thesis: (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq9_/"_seq)_(#)_(seq19_/"_seq1))_._n_=_((seq9_(#)_seq19)_/"_(seq_(#)_seq1))_._n let n be Element of NAT ; ::_thesis: ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) seq19) /" (seq (#) seq1)) . n thus ((seq9 /" seq) (#) (seq19 /" seq1)) . n = ((seq9 (#) (seq ")) . n) * ((seq19 /" seq1) . n) by VALUED_1:5 .= ((seq9 . n) * ((seq ") . n)) * ((seq19 (#) (seq1 ")) . n) by VALUED_1:5 .= ((seq9 . n) * ((seq ") . n)) * ((seq19 . n) * ((seq1 ") . n)) by VALUED_1:5 .= (seq9 . n) * ((seq19 . n) * (((seq ") . n) * ((seq1 ") . n))) .= (seq9 . n) * ((seq19 . n) * (((seq ") (#) (seq1 ")) . n)) by VALUED_1:5 .= ((seq9 . n) * (seq19 . n)) * (((seq ") (#) (seq1 ")) . n) .= ((seq9 . n) * (seq19 . n)) * (((seq (#) seq1) ") . n) by Th30 .= ((seq9 (#) seq19) . n) * (((seq (#) seq1) ") . n) by VALUED_1:5 .= ((seq9 (#) seq19) /" (seq (#) seq1)) . n by VALUED_1:5 ; ::_thesis: verum end; hence (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1) by FUNCT_2:63; ::_thesis: verum 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 proof let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is non-zero & seq1 is non-zero implies seq /" seq1 is non-zero ) assume that A1: seq is non-zero and A2: seq1 is non-zero ; ::_thesis: seq /" seq1 is non-zero seq1 " is non-zero by A2, Th27; hence seq /" seq1 is non-zero by A1, Th29; ::_thesis: verum end; theorem Th34: :: COMSEQ_1:34 for seq, seq1 being Complex_Sequence holds (seq /" seq1) " = seq1 /" seq proof let seq, seq1 be Complex_Sequence; ::_thesis: (seq /" seq1) " = seq1 /" seq now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_/"_seq1)_")_._n_=_(seq1_/"_seq)_._n let n be Element of NAT ; ::_thesis: ((seq /" seq1) ") . n = (seq1 /" seq) . n thus ((seq /" seq1) ") . n = ((seq ") (#) ((seq1 ") ")) . n by Th30 .= (seq1 /" seq) . n ; ::_thesis: verum end; hence (seq /" seq1) " = seq1 /" seq by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_1:35 for seq2, seq1, seq being Complex_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq proof let seq2, seq1, seq be Complex_Sequence; ::_thesis: seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq thus seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) (#) (seq ") by Th8 .= (seq2 (#) seq1) /" seq ; ::_thesis: verum end; theorem :: COMSEQ_1:36 for seq2, seq, seq1 being Complex_Sequence holds seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq proof let seq2, seq, seq1 be Complex_Sequence; ::_thesis: seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq2_/"_(seq_/"_seq1))_._n_=_((seq2_(#)_seq1)_/"_seq)_._n let n be Element of NAT ; ::_thesis: (seq2 /" (seq /" seq1)) . n = ((seq2 (#) seq1) /" seq) . n thus (seq2 /" (seq /" seq1)) . n = (seq2 (#) (seq1 /" seq)) . n by Th34 .= ((seq2 (#) seq1) (#) (seq ")) . n by Th8 .= ((seq2 (#) seq1) /" seq) . n ; ::_thesis: verum end; hence seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq by FUNCT_2:63; ::_thesis: verum end; theorem Th37: :: COMSEQ_1:37 for seq1, seq2, seq being Complex_Sequence st seq1 is non-zero holds seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) proof let seq1, seq2, seq be Complex_Sequence; ::_thesis: ( seq1 is non-zero implies seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) ) assume A1: seq1 is non-zero ; ::_thesis: seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq2_/"_seq)_._n_=_((seq2_(#)_seq1)_/"_(seq_(#)_seq1))_._n let n be Element of NAT ; ::_thesis: (seq2 /" seq) . n = ((seq2 (#) seq1) /" (seq (#) seq1)) . n A2: seq1 . n <> 0c by A1, Th4; thus (seq2 /" seq) . n = ((seq2 . n) * 1r) * ((seq ") . n) by VALUED_1:5 .= ((seq2 . n) * ((seq1 . n) * ((seq1 . n) "))) * ((seq ") . n) by A2, XCMPLX_0:def_7 .= ((seq2 . n) * (seq1 . n)) * (((seq1 . n) ") * ((seq ") . n)) .= ((seq2 (#) seq1) . n) * (((seq1 . n) ") * ((seq ") . n)) by VALUED_1:5 .= ((seq2 (#) seq1) . n) * (((seq1 ") . n) * ((seq ") . n)) by VALUED_1:10 .= ((seq2 (#) seq1) . n) * (((seq ") (#) (seq1 ")) . n) by VALUED_1:5 .= ((seq2 (#) seq1) . n) * (((seq (#) seq1) ") . n) by Th30 .= ((seq2 (#) seq1) /" (seq (#) seq1)) . n by VALUED_1:5 ; ::_thesis: verum end; hence seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1) by FUNCT_2:63; ::_thesis: verum end; theorem Th38: :: COMSEQ_1:38 for r being Element of COMPLEX for seq being Complex_Sequence st r <> 0c & seq is non-zero holds r (#) seq is non-zero proof let r be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence st r <> 0c & seq is non-zero holds r (#) seq is non-zero let seq be Complex_Sequence; ::_thesis: ( r <> 0c & seq is non-zero implies r (#) seq is non-zero ) assume that A1: r <> 0c and A2: seq is non-zero and A3: not r (#) seq is non-zero ; ::_thesis: contradiction consider n1 being Element of NAT such that A4: (r (#) seq) . n1 = 0c by A3, Th4; A5: r * (seq . n1) = 0c by A4, VALUED_1:6; seq . n1 <> 0c by A2, Th4; hence contradiction by A1, A5; ::_thesis: verum end; theorem :: COMSEQ_1:39 for seq being Complex_Sequence st seq is non-zero holds - seq is non-zero proof let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies - seq is non-zero ) A1: - (- 1r) = 1r ; assume seq is non-zero ; ::_thesis: - seq is non-zero hence - seq is non-zero by A1, Th38; ::_thesis: verum end; theorem Th40: :: COMSEQ_1:40 for r being Element of COMPLEX for seq being Complex_Sequence holds (r (#) seq) " = (r ") (#) (seq ") proof let r be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence holds (r (#) seq) " = (r ") (#) (seq ") let seq be Complex_Sequence; ::_thesis: (r (#) seq) " = (r ") (#) (seq ") now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_seq)_")_._n_=_((r_")_(#)_(seq_"))_._n let n be Element of NAT ; ::_thesis: ((r (#) seq) ") . n = ((r ") (#) (seq ")) . n thus ((r (#) seq) ") . n = ((r (#) seq) . n) " by VALUED_1:10 .= (r * (seq . n)) " by VALUED_1:6 .= (r ") * ((seq . n) ") by XCMPLX_1:204 .= (r ") * ((seq ") . n) by VALUED_1:10 .= ((r ") (#) (seq ")) . n by VALUED_1:6 ; ::_thesis: verum end; hence (r (#) seq) " = (r ") (#) (seq ") by FUNCT_2:63; ::_thesis: verum end; theorem Th41: :: COMSEQ_1:41 for seq being Complex_Sequence st seq is non-zero holds (- seq) " = (- 1r) (#) (seq ") proof let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies (- seq) " = (- 1r) (#) (seq ") ) (- 1) " = - 1 ; hence ( seq is non-zero implies (- seq) " = (- 1r) (#) (seq ") ) by Th40; ::_thesis: verum end; theorem :: COMSEQ_1:42 for seq, seq1 being Complex_Sequence st seq is non-zero holds ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) ) proof let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is non-zero implies ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) ) ) assume A1: seq is non-zero ; ::_thesis: ( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) ) thus - (seq1 /" seq) = (- 1r) (#) (seq1 /" seq) .= ((- 1r) (#) seq1) (#) (seq ") by Th12 .= (- seq1) /" seq ; ::_thesis: seq1 /" (- seq) = - (seq1 /" seq) thus seq1 /" (- seq) = seq1 (#) ((- 1r) (#) (seq ")) by A1, Th41 .= (- 1r) (#) (seq1 (#) (seq ")) by Th13 .= - (seq1 /" seq) ; ::_thesis: verum end; theorem :: COMSEQ_1:43 for seq1, seq, seq19 being Complex_Sequence holds ( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq ) proof let seq1, seq, seq19 be Complex_Sequence; ::_thesis: ( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq ) thus (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) (#) (seq ") by Th9 .= (seq1 + seq19) /" seq ; ::_thesis: (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq thus (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) (#) (seq ") by Th14 .= (seq1 - seq19) /" seq ; ::_thesis: verum end; theorem :: COMSEQ_1:44 for seq, seq9, seq1, 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) ) proof let seq, seq9, seq1, seq19 be Complex_Sequence; ::_thesis: ( seq is non-zero & seq9 is non-zero implies ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ) ) assume that A1: seq is non-zero and A2: seq9 is non-zero ; ::_thesis: ( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ) thus (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) + (seq19 /" seq9) by A2, Th37 .= ((seq1 (#) seq9) /" (seq (#) seq9)) + ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th37 .= ((seq1 (#) seq9) + (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th9 .= ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) ; ::_thesis: (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) thus (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) /" (seq (#) seq9)) - (seq19 /" seq9) by A2, Th37 .= ((seq1 (#) seq9) /" (seq (#) seq9)) - ((seq19 (#) seq) /" (seq (#) seq9)) by A1, Th37 .= ((seq1 (#) seq9) - (seq19 (#) seq)) (#) ((seq (#) seq9) ") by Th14 .= ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) ; ::_thesis: verum end; theorem :: COMSEQ_1:45 for seq19, seq, seq9, seq1 being Complex_Sequence holds (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9) proof let seq19, seq, seq9, seq1 be Complex_Sequence; ::_thesis: (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9) thus (seq19 /" seq) /" (seq9 /" seq1) = (seq19 /" seq) (#) ((seq9 ") (#) ((seq1 ") ")) by Th30 .= ((seq19 (#) (seq ")) (#) seq1) (#) (seq9 ") by Th8 .= (seq19 (#) (seq1 (#) (seq "))) (#) (seq9 ") by Th8 .= seq19 (#) ((seq1 (#) (seq ")) (#) (seq9 ")) by Th8 .= seq19 (#) (seq1 (#) ((seq ") (#) (seq9 "))) by Th8 .= (seq19 (#) seq1) (#) ((seq ") (#) (seq9 ")) by Th8 .= (seq19 (#) seq1) /" (seq (#) seq9) by Th30 ; ::_thesis: verum end; theorem Th46: :: COMSEQ_1:46 for seq, seq9 being Complex_Sequence holds |.(seq (#) seq9).| = |.seq.| (#) |.seq9.| proof let seq, seq9 be Complex_Sequence; ::_thesis: |.(seq (#) seq9).| = |.seq.| (#) |.seq9.| now__::_thesis:_for_n_being_Element_of_NAT_holds_|.(seq_(#)_seq9).|_._n_=_(|.seq.|_(#)_|.seq9.|)_._n let n be Element of NAT ; ::_thesis: |.(seq (#) seq9).| . n = (|.seq.| (#) |.seq9.|) . n thus |.(seq (#) seq9).| . n = |.((seq (#) seq9) . n).| by VALUED_1:18 .= |.((seq . n) * (seq9 . n)).| by VALUED_1:5 .= |.(seq . n).| * |.(seq9 . n).| by COMPLEX1:65 .= (|.seq.| . n) * |.(seq9 . n).| by VALUED_1:18 .= (|.seq.| . n) * (|.seq9.| . n) by VALUED_1:18 .= (|.seq.| (#) |.seq9.|) . n by VALUED_1:5 ; ::_thesis: verum end; hence |.(seq (#) seq9).| = |.seq.| (#) |.seq9.| by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_1:47 for seq being Complex_Sequence st seq is non-zero holds |.seq.| is non-zero proof let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies |.seq.| is non-zero ) assume A1: seq is non-zero ; ::_thesis: |.seq.| is non-zero now__::_thesis:_for_n_being_Element_of_NAT_holds_|.seq.|_._n_<>_0 let n be Element of NAT ; ::_thesis: |.seq.| . n <> 0 seq . n <> 0c by A1, Th4; then |.(seq . n).| <> 0 by COMPLEX1:45; hence |.seq.| . n <> 0 by VALUED_1:18; ::_thesis: verum end; hence |.seq.| is non-zero by SEQ_1:5; ::_thesis: verum end; theorem Th48: :: COMSEQ_1:48 for seq being Complex_Sequence holds |.seq.| " = |.(seq ").| proof let seq be Complex_Sequence; ::_thesis: |.seq.| " = |.(seq ").| now__::_thesis:_for_n_being_Element_of_NAT_holds_|.(seq_").|_._n_=_(|.seq.|_")_._n let n be Element of NAT ; ::_thesis: |.(seq ").| . n = (|.seq.| ") . n thus |.(seq ").| . n = |.((seq ") . n).| by VALUED_1:18 .= |.((seq . n) ").| by VALUED_1:10 .= |.(1r / (seq . n)).| by XCMPLX_1:215 .= 1 / |.(seq . n).| by COMPLEX1:48, COMPLEX1:67 .= |.(seq . n).| " by XCMPLX_1:215 .= (|.seq.| . n) " by VALUED_1:18 .= (|.seq.| ") . n by VALUED_1:10 ; ::_thesis: verum end; hence |.seq.| " = |.(seq ").| by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_1:49 for seq9, seq being Complex_Sequence holds |.(seq9 /" seq).| = |.seq9.| /" |.seq.| proof let seq9, seq be Complex_Sequence; ::_thesis: |.(seq9 /" seq).| = |.seq9.| /" |.seq.| thus |.(seq9 /" seq).| = |.seq9.| (#) |.(seq ").| by Th46 .= |.seq9.| /" |.seq.| by Th48 ; ::_thesis: verum end; theorem :: COMSEQ_1:50 for r being Element of COMPLEX for seq being Complex_Sequence holds |.(r (#) seq).| = |.r.| (#) |.seq.| proof let r be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence holds |.(r (#) seq).| = |.r.| (#) |.seq.| let seq be Complex_Sequence; ::_thesis: |.(r (#) seq).| = |.r.| (#) |.seq.| now__::_thesis:_for_n_being_Element_of_NAT_holds_|.(r_(#)_seq).|_._n_=_(|.r.|_(#)_|.seq.|)_._n let n be Element of NAT ; ::_thesis: |.(r (#) seq).| . n = (|.r.| (#) |.seq.|) . n thus |.(r (#) seq).| . n = |.((r (#) seq) . n).| by VALUED_1:18 .= |.(r * (seq . n)).| by VALUED_1:6 .= |.r.| * |.(seq . n).| by COMPLEX1:65 .= |.r.| * (|.seq.| . n) by VALUED_1:18 .= (|.r.| (#) |.seq.|) . n by VALUED_1:6 ; ::_thesis: verum end; hence |.(r (#) seq).| = |.r.| (#) |.seq.| by FUNCT_2:63; ::_thesis: verum end;