theorem :: VECTSP_2:12

for SF being Skew-Field
for x, y being Scalar of SF holds
( not x * y = 0. SF or x = 0. SF or y = 0. SF )