let i be Nat; :: thesis: for c being Complex holds - (i |-> c) = i |-> (- c)
let c be Complex; :: thesis: - (i |-> c) = i |-> (- c)
reconsider s = c as Element of COMPLEX by XCMPLX_0:def 2;
- (i |-> s) = i |-> (compcomplex . s) by FINSEQOP:16
.= i |-> (- c) by BINOP_2:def 1 ;
hence - (i |-> c) = i |-> (- c) ; :: thesis: verum