let F be non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for x being Element of F st x <> 0. F holds

(x ") " = x

let x be Element of F; :: thesis: ( x <> 0. F implies (x ") " = x )

assume A1: x <> 0. F ; :: thesis: (x ") " = x

( x <> 0. F implies x " <> 0. F )

then (x * (x ")) * ((x ") ") = x * (1. F) by GROUP_1:def 3;

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

then (x ") " = x * (1. F) ;

hence (x ") " = x ; :: thesis: verum

(x ") " = x

let x be Element of F; :: thesis: ( x <> 0. F implies (x ") " = x )

assume A1: x <> 0. F ; :: thesis: (x ") " = x

( x <> 0. F implies x " <> 0. F )

proof

then
(x ") * ((x ") ") = 1. F
by A1, Def10;
assume A2:
x <> 0. F
; :: thesis: x " <> 0. F

assume not x " <> 0. F ; :: thesis: contradiction

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

hence contradiction ; :: thesis: verum

end;assume not x " <> 0. F ; :: thesis: contradiction

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

hence contradiction ; :: thesis: verum

then (x * (x ")) * ((x ") ") = x * (1. F) by GROUP_1:def 3;

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

then (x ") " = x * (1. F) ;

hence (x ") " = x ; :: thesis: verum