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:82;
then (a " ) |^ (ord a) = 1_ G by Th3;
then A1: ord (a " ) divides ord a by GROUP_1:86;
(a " ) |^ (ord (a " )) = 1_ G by GROUP_1:82;
then a |^ (ord (a " )) = 1_ G by Th4;
then ord a divides ord (a " ) by GROUP_1:86;
hence ord (a " ) = ord a by A1, NAT_D:5; :: thesis: verum