let F be Field; :: thesis: for x being Element of F st x <> 0. F holds
( x " <> 0. F & - (x ") <> 0. F )
let x be Element of F; :: thesis: ( x <> 0. F implies ( x " <> 0. F & - (x ") <> 0. F ) )
assume A1: x <> 0. F ; :: thesis: ( x " <> 0. F & - (x ") <> 0. F )

hereby :: thesis: - (x ") <> 0. F

assume x " = 0. F ; :: thesis: contradiction
then 1. F = x * (0. F) by A1, Def10;
hence contradiction ; :: thesis: verum

end;

assume - (x ") = 0. F ; :: thesis: contradiction
then (1. F) * (x ") = (- (1. F)) * (0. F) by Th6;
then x * (x ") = x * (0. F) ;
then 1. F = x * (0. F) by A1, Def10;
hence contradiction ; :: thesis: verum