theorem :: VECTSP_1:25

for F being Field
for x being Element of F st x <> 0. F holds
( x " <> 0. F & - (x ") <> 0. F )