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