let x, y be Element of (MultGroup F); :: according to GROUP_1:def 16 :: thesis: x * y = y * x
( x in the carrier of (MultGroup F) & y in the carrier of (MultGroup F) ) ;
then A1: ( x in NonZero F & y in NonZero F ) by UNIROOTS:def 1;
then reconsider x1 = x as Element of F ;
reconsider y1 = y as Element of F by A1;
x * y = x1 * y1 by UNIROOTS:19
.= y * x by UNIROOTS:19 ;
hence x * y = y * x ; :: thesis: verum