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

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 by VECTSP_1:def 4;
hence h * uR = h by Th19; :: thesis: uR * h = h
(1_ R) * g = g by VECTSP_1:def 8;
hence uR * h = h by Th19; :: thesis: verum

end;

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