let seq, seq1 be Real_Sequence; :: thesis: ( seq is V8() & 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 V8() 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:20
.= (seq . 0 ) + (lim seq1) by A1, Th40 ; :: 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:26
.= (seq . 0 ) - (lim seq1) by A1, Th40 ; :: 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:26
.= (lim seq1) - (seq . 0 ) by A1, Th40 ; :: thesis: lim (seq (#) seq1) = (seq . 0 ) * (lim seq1)
thus lim (seq (#) seq1) = (lim seq) * (lim seq1) by A1, A2, SEQ_2:29
.= (seq . 0 ) * (lim seq1) by A1, Th40 ; :: thesis: verum