let G be Group; :: thesis: for a being Element of G holds ord (a ") = ord a
let a be Element of G; :: thesis: ord (a ") = ord a
a |^ (ord a) = 1_ G by GROUP_1:41;
then (a ") |^ (ord a) = 1_ G by Th3;
then A1: ord (a ") divides ord a by GROUP_1:44;
(a ") |^ (ord (a ")) = 1_ G by GROUP_1:41;
then a |^ (ord (a ")) = 1_ G by Th4;
then ord a divides ord (a ") by GROUP_1:44;
hence ord (a ") = ord a by A1, NAT_D:5; :: thesis: verum