let seq, seq1 be Real_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) )
thus lim (seq + seq1) = (lim seq) + (lim seq1) by A1, A2, SEQ_2:6
.= (seq . 0) + (lim seq1) by A1, Th25 ; :: 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 A1, A2, SEQ_2:12
.= (seq . 0) - (lim seq1) by A1, Th25 ; :: thesis: ( lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
thus lim (seq1 - seq) = (lim seq1) - (lim seq) by A1, A2, SEQ_2:12
.= (lim seq1) - (seq . 0) by A1, Th25 ; :: thesis: lim (seq (#) seq1) = (seq . 0) * (lim seq1)
thus lim (seq (#) seq1) = (lim seq) * (lim seq1) by A1, A2, SEQ_2:15
.= (seq . 0) * (lim seq1) by A1, Th25 ; :: thesis: verum