let x, y be Element of (MultGroup F); :: according to GROUP_1:def 12 :: thesis: x * y = y * x

x in the carrier of (MultGroup F) ;

then x in NonZero F by UNIROOTS:def 1;

then reconsider x1 = x as Element of F ;

y in the carrier of (MultGroup F) ;

then y in NonZero F by UNIROOTS:def 1;

then reconsider y1 = y as Element of F ;

x * y = x1 * y1 by UNIROOTS:16

.= y * x by UNIROOTS:16 ;

hence x * y = y * x ; :: thesis: verum

x in the carrier of (MultGroup F) ;

then x in NonZero F by UNIROOTS:def 1;

then reconsider x1 = x as Element of F ;

y in the carrier of (MultGroup F) ;

then y in NonZero F by UNIROOTS:def 1;

then reconsider y1 = y as Element of F ;

x * y = x1 * y1 by UNIROOTS:16

.= y * x by UNIROOTS:16 ;

hence x * y = y * x ; :: thesis: verum