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 Th48;
(x ") " = ((x ") ") * (1_ SF) by VECTSP_1:def 4
.= ((x ") ") * ((x ") * x) by A1, Th43
.= (((x ") ") * (x ")) * x by GROUP_1:def 3 ;
then (x ") " = (1_ SF) * x by A2, Th43;
hence (x ") " = x by VECTSP_1:def 8; :: thesis: verum