let SF be Skew-Field; :: thesis: for x being Scalar of SF st x <> 0. SF holds
( (1_ SF) / x = x " & (1_ SF) / (x ") = x )
let x be Scalar of SF; :: thesis: ( x <> 0. SF implies ( (1_ SF) / x = x " & (1_ SF) / (x ") = x ) )
( x <> 0. SF implies (1_ SF) / (x ") = x )

proof

assume A1: x <> 0. SF ; :: thesis: (1_ SF) / (x ") = x
(1_ SF) / (x ") = (x ") " by VECTSP_1:def 8
.= x by A1, Th49 ;
hence (1_ SF) / (x ") = x ; :: thesis: verum

end;

hence ( x <> 0. SF implies ( (1_ SF) / x = x " & (1_ SF) / (x ") = x ) ) by VECTSP_1:def 8; :: thesis: verum