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