let R be Skew-Field; :: thesis: the carrier of R = the carrier of (MultGroup R) \/ {(0. R)}
NonZero R = the carrier of (MultGroup R) by Def1;
hence the carrier of R = the carrier of (MultGroup R) \/ {(0. R)} by XBOOLE_1:45; :: thesis: verum