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:3
.= (- 1r) (#) (seq_id u) by Lm13
.= - (seq_id u) by COMSEQ_1:11 ;
hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ; :: thesis: verum