let F be commutative Skew-Field; :: thesis: for x being Element of (MultGroup F)
for x1 being Element of F st x = x1 holds
x " = x1 "
let h be Element of (MultGroup F); :: thesis: for x1 being Element of F st h = x1 holds
h " = x1 "
let hp be Element of F; :: thesis: ( h = hp implies h " = hp " )
assume A1: h = hp ; :: thesis: h " = hp "
set hpd = hp " ;
h in the carrier of (MultGroup F) ;
then h in NonZero F by UNIROOTS:def 1;
then not h in {(0. F)} by XBOOLE_0:def 5;
then A2: h <> 0. F by TARSKI:def 1;
then hp * (hp ") = 1. F by A1, VECTSP_1:def 10;
then hp " <> 0. F ;
then not hp " in {(0. F)} by TARSKI:def 1;
then hp " in NonZero F by XBOOLE_0:def 5;
then reconsider g = hp " as Element of (MultGroup F) by UNIROOTS:def 1;
A3: 1_ F = 1_ (MultGroup F) by UNIROOTS:17;
g * h = (hp ") * hp by A1, UNIROOTS:16
.= 1_ (MultGroup F) by A1, A2, A3, VECTSP_1:def 10 ;
hence h " = hp " by GROUP_1:def 5; :: thesis: verum