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