assume A1: p = f ; :: thesis: - p = - f
thus - p = (- 1) * p by RLVECT_1:16
.= - f by A1 ; :: thesis: verum