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;

now :: thesis: for h being Element of (MultGroup R) holds
( 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;

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