theorem YY: :: REALALG2:12

for F being Field
for a being non zero Element of F holds (- (a ")) " = - a