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