let u be VECTOR of Complex_l2_Space ; :: thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1r ) * u by CLVECT_1:4
.= (- 1r ) (#) (seq_id u) by Lm14
.= - (seq_id u) by COMSEQ_1:14 ;
hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by Lm12; :: thesis: verum