let G be Group; :: thesis: for a, b being Element of G holds ord (a |^ b) = ord a
let a, b be Element of G; :: thesis: ord (a |^ b) = ord a
(a |^ b) |^ (ord a) = (a |^ (ord a)) |^ b by GROUP_3:33
.= (1_ G) |^ b by GROUP_1:82
.= 1_ G by GROUP_3:22 ;
then A2: ord (a |^ b) divides ord a by GROUP_1:86;
(a |^ (ord (a |^ b))) |^ b = (a |^ b) |^ (ord (a |^ b)) by GROUP_3:33
.= 1_ G by GROUP_1:82 ;
then ord a divides ord (a |^ b) by GROUP_3:23, GROUP_1:86;
hence ord (a |^ b) = ord a by A2, NAT_D:5; :: thesis: verum