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 )

proof

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;

then (x ") * ((x ") ") = 1. F by A1, Def10;
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