let SF be Skew-Field; :: thesis: for x being Scalar of SF st x <> 0. SF holds
( x * ((1_ SF) / x) = 1_ SF & ((1_ SF) / x) * x = 1_ SF )
let x be Scalar of SF; :: thesis: ( x <> 0. SF implies ( x * ((1_ SF) / x) = 1_ SF & ((1_ SF) / x) * x = 1_ SF ) )
assume A1: x <> 0. SF ; :: thesis: ( x * ((1_ SF) / x) = 1_ SF & ((1_ SF) / x) * x = 1_ SF )
hence x * ((1_ SF) / x) = x * (x " ) by Th50
.= 1_ SF by A1, Th43 ;
:: thesis: ((1_ SF) / x) * x = 1_ SF
thus ((1_ SF) / x) * x = (x " ) * x by A1, Th50
.= 1_ SF by A1, Th43 ; :: thesis: verum