let G be Group; :: thesis: for H being Subgroup of G
for a being Element of H
for b being Element of G st a = b & G is finite holds
ord a = ord b
let H be Subgroup of G; :: thesis: for a being Element of H
for b being Element of G st a = b & G is finite holds
ord a = ord b
let a be Element of H; :: thesis: for b being Element of G st a = b & G is finite holds
ord a = ord b
let b be Element of G; :: thesis: ( a = b & G is finite implies ord a = ord b )
assume A1: ( a = b & G is finite ) ; :: thesis: ord a = ord b
A2: ( not a is being_of_order_0 & not b is being_of_order_0 ) by A1, GR_CY_1:26;
then A3: a |^ (ord a) = 1_ H by GROUP_1:def 12;
A4: b |^ (ord b) = 1_ G by A2, GROUP_1:def 12;
a |^ (ord a) = b |^ (ord a) by A1, GROUP_4:3;
then A5: ord b divides ord a by A3, A4, GROUP_1:86, GROUP_2:53;
a |^ (ord b) = 1_ G by A1, A4, GROUP_4:3;
then a |^ (ord b) = 1_ H by GROUP_2:53;
then ord a divides ord b by GROUP_1:86;
hence ord a = ord b by A5, NAT_D:5; :: thesis: verum