theorem Th22: :: VECTSP_1:26

(1. F_Real) + (1. F_Real) <> 0. F_Real ;