let a be Element of G_Real; :: according to VECTSP_1:def 18 :: thesis: ( not a # a = 0. G_Real or a = 0. G_Real )
assume a + a = 0. G_Real ; :: thesis: a = 0. G_Real
hence a = 0. G_Real ; :: thesis: verum