let x be FinSequence of COMPLEX ; :: thesis: - (0c (len x)) = 0c (len x)
- (0c (len x)) = - ((len x) |-> 0c ) by SEQ_4:def 15
.= compcomplex * ((len x) |-> 0c ) by SEQ_4:def 11
.= (len x) |-> (compcomplex . 0c ) by FINSEQOP:17
.= (len x) |-> (- 0c ) by BINOP_2:def 1
.= 0c (len x) by SEQ_4:def 15 ;
hence - (0c (len x)) = 0c (len x) ; :: thesis: verum