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 :: thesis: ( x * y = 0. SF & x <> 0. SF implies y = 0. SF )

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

end;

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