let SF be Skew-Field; :: thesis: for x being Scalar of SF st x <> 0. SF holds
x " <> 0. SF
let x be Scalar of SF; :: thesis: ( x <> 0. SF implies x " <> 0. SF )
assume A1: x <> 0. SF ; :: thesis: x " <> 0. SF
assume x " = 0. SF ; :: thesis: contradiction
then x * (x ") = 0. SF ;
then 1. SF = 0. SF by A1, Th9;
hence contradiction ; :: thesis: verum