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

now

assume that
A1: x * y = 0. SF and
A2: x <> 0. SF ; :: thesis: y = 0. SF
x * y = x * (0. SF) by A1, VECTSP_1:6;
hence y = 0. SF by A2, Th42; :: thesis: verum

end;

hence ( not x * y = 0. SF or x = 0. SF or y = 0. SF ) ; :: thesis: verum