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:27
.= (1_ G) |^ b by GROUP_1:41
.= 1_ G by GROUP_3:17 ;
then A1: ord (a |^ b) divides ord a by GROUP_1:44;
(a |^ (ord (a |^ b))) |^ b = (a |^ b) |^ (ord (a |^ b)) by GROUP_3:27
.= 1_ G by GROUP_1:41 ;
then ord a divides ord (a |^ b) by GROUP_1:44, GROUP_3:18;
hence ord (a |^ b) = ord a by A1, NAT_D:5; :: thesis: verum