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