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 )

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

( 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: contradictionassume
x " = 0. F
; :: thesis: contradiction

then 1. F = x * (0. F) by A1, Def10;

hence contradiction ; :: thesis: verum

end;then 1. F = x * (0. F) by A1, Def10;

hence contradiction ; :: thesis: verum

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