let x, y be Element of (PrimeField F); :: according to GROUP_1:def 12 :: thesis: x * y = y * x
reconsider a = x, b = y as Element of F by Lm10;
thus x * y = a * b by Lm12
.= y * x by Lm12 ; :: thesis: verum