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