let R be Skew-Field; :: thesis: 1_ R = 1_ (MultGroup R)

A1: the carrier of (MultGroup R) = NonZero R by Def1;

not 1_ R in {(0. R)} by TARSKI:def 1;

then reconsider uR = 1_ R as Element of (MultGroup R) by A1, XBOOLE_0:def 5;

A1: the carrier of (MultGroup R) = NonZero R by Def1;

not 1_ R in {(0. R)} by TARSKI:def 1;

then reconsider uR = 1_ R as Element of (MultGroup R) by A1, XBOOLE_0:def 5;

now :: thesis: for h being Element of (MultGroup R) holds

( h * uR = h & uR * h = h )

hence
1_ R = 1_ (MultGroup R)
by GROUP_1:def 4; :: thesis: verum( h * uR = h & uR * h = h )

let h be Element of (MultGroup R); :: thesis: ( h * uR = h & uR * h = h )

reconsider g = h as Element of R by A1, XBOOLE_0:def 5;

g * (1_ R) = g ;

hence h * uR = h by Th16; :: thesis: uR * h = h

(1_ R) * g = g ;

hence uR * h = h by Th16; :: thesis: verum

end;reconsider g = h as Element of R by A1, XBOOLE_0:def 5;

g * (1_ R) = g ;

hence h * uR = h by Th16; :: thesis: uR * h = h

(1_ R) * g = g ;

hence uR * h = h by Th16; :: thesis: verum