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 )
A1: ( 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, Def22;
hence contradiction by Th39; :: thesis: verum

end;

assume A3: x <> 0. F ; :: thesis: (x " ) " = x
then (x " ) * ((x " ) " ) = 1. F by A1, Def22;
then (x * (x " )) * ((x " ) " ) = x * (1. F) by GROUP_1:def 4;
then (1. F) * ((x " ) " ) = x * (1. F) by A3, Def22;
then (x " ) " = x * (1. F) by Def16;
hence (x " ) " = x by Def16; :: thesis: verum