reconsider w = - y as Element of F_Rat by RAT_1:def 2;
assume x = y ; :: thesis: - x = - y
then x + w = 0. F_Rat ;
hence - x = - y by VECTSP_1:16; :: thesis: verum