let i be natural Number ; :: thesis: for r being Real holds - (i |-> r) = i |-> (- r)
let r be Real; :: thesis: - (i |-> r) = i |-> (- r)
reconsider s = r as Element of REAL by XREAL_0:def 1;
- (i |-> s) = i |-> (compreal . s) by FINSEQOP:16
.= i |-> (- r) by BINOP_2:def 7 ;
hence - (i |-> r) = i |-> (- r) ; :: thesis: verum