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 Th19
.= (r (#) seq1) + (r (#) ((- 1r ) (#) seq2))
.= (r (#) seq1) + (((- 1r ) * r) (#) seq2) by Th20
.= (r (#) seq1) + ((- 1r ) (#) (r (#) seq2)) by Th20
.= (r (#) seq1) - (r (#) seq2) ; :: thesis: verum