let seq, seq1 be Complex_Sequence; :: thesis: ( seq is constant & seq1 is convergent implies ( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) ) )
assume that
A1: seq is constant and
A2: seq1 is convergent ; :: thesis: ( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
A3: seq is convergent by A1, Th26;
hence lim (seq + seq1) = (lim seq) + (lim seq1) by A2, COMSEQ_2:14
.= (seq . 0) + (lim seq1) by A1, Th27 ;
:: thesis: ( lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
thus lim (seq - seq1) = (lim seq) - (lim seq1) by A2, A3, COMSEQ_2:26
.= (seq . 0) - (lim seq1) by A1, Th27 ; :: thesis: ( lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
thus lim (seq1 - seq) = (lim seq1) - (lim seq) by A2, A3, COMSEQ_2:26
.= (lim seq1) - (seq . 0) by A1, Th27 ; :: thesis: lim (seq (#) seq1) = (seq . 0) * (lim seq1)
thus lim (seq (#) seq1) = (lim seq) * (lim seq1) by A2, A3, COMSEQ_2:30
.= (seq . 0) * (lim seq1) by A1, Th27 ; :: thesis: verum