theorem :: EUCLID:68

for n being Nat
for p1 being Point of (TOP-REAL n)
for r1 being real-valued Function st p1 = r1 holds
- p1 = - r1 ;