convergent for Complex_Sequence; end; ::$CT theorem :: COMSEQ_2:12 s is convergent implies lim(s*') = (lim s)*'; begin :: Main Theorems registration let s1,s2 be convergent Complex_Sequence; cluster s1 + s2 -> convergent for Complex_Sequence; end; ::$CT theorem :: COMSEQ_2:14 for s,s9 being convergent Complex_Sequence holds lim (s + s9)=(lim s)+ (lim s9); ::$CT theorem :: COMSEQ_2:16 for s,s9 being convergent Complex_Sequence holds lim (s + s9)*' = (lim s)*' + (lim s9)*'; registration let s be convergent Complex_Sequence, c be Complex; cluster c(#)s -> convergent for Complex_Sequence; end; ::$CT theorem :: COMSEQ_2:18 for s being convergent Complex_Sequence, r being Complex holds lim(r(#)s)=r*(lim s); ::$CT theorem :: COMSEQ_2:20 for s being convergent Complex_Sequence holds lim (r(#)s)*' = (r*')*(lim s)*'; registration let s be convergent Complex_Sequence; cluster -s -> convergent for Complex_Sequence; end; ::$CT theorem :: COMSEQ_2:22 for s being convergent Complex_Sequence holds lim(-s)=-(lim s); ::$CT theorem :: COMSEQ_2:24 for s being convergent Complex_Sequence holds lim (-s)*' = -(lim s)*'; registration let s1,s2 be convergent Complex_Sequence; cluster s1 - s2 -> convergent for Complex_Sequence; end; ::$CT theorem :: COMSEQ_2:26 for s,s9 being convergent Complex_Sequence holds lim(s - s9)=(lim s)-( lim s9); ::$CT theorem :: COMSEQ_2:28 for s,s9 being convergent Complex_Sequence holds lim (s - s9)*' = (lim s)*' - (lim s9)*'; registration cluster convergent -> bounded for Complex_Sequence; end; registration cluster non bounded -> non convergent for Complex_Sequence; end; registration let s1,s2 be convergent Complex_Sequence; cluster s1 (#) s2 -> convergent for Complex_Sequence; end; ::$CT theorem :: COMSEQ_2:30 for s,s9 being convergent Complex_Sequence holds lim(s(#)s9)=(lim s)*(lim s9); ::$CT theorem :: COMSEQ_2:32 for s,s9 being convergent Complex_Sequence holds lim (s(#)s9)*' = (lim s)*' * (lim s9)*'; theorem :: COMSEQ_2:33 for s being convergent Complex_Sequence st lim s <> 0c ex n st for m st n <=m holds |.(lim s).|/2<|.s.m.|; theorem :: COMSEQ_2:34 for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds s" is convergent; theorem :: COMSEQ_2:35 s is convergent & (lim s)<>0c & s is non-zero implies lim s"=( lim s)"; ::$CT theorem :: COMSEQ_2:37 s is convergent & (lim s)<>0c & s is non-zero implies lim (s")*' = (( lim s)*')"; theorem :: COMSEQ_2:38 s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies s9/"s is convergent; theorem :: COMSEQ_2:39 s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim(s9/"s)=(lim s9)/(lim s); ::$CT theorem :: COMSEQ_2:41 s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim (s9/"s)*' = ((lim s9)*')/((lim s)*'); theorem :: COMSEQ_2:42 s is convergent & s1 is bounded & (lim s)=0c implies s(#)s1 is convergent; theorem :: COMSEQ_2:43 s is convergent & s1 is bounded & (lim s)=0c implies lim(s(#)s1) =0c; ::$CT theorem :: COMSEQ_2:45 s is convergent & s1 is bounded & (lim s)=0c implies lim (s(#)s1)*' = 0c;