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 that
A1: a = b and
A2: G is finite ; :: thesis: ord a = ord b
A3: not a is being_of_order_0 by A2, GR_CY_1:6;
A4: not b is being_of_order_0 by A2, GR_CY_1:6;
A5: a |^ (ord a) = 1_ H by A3, GROUP_1:def 11;
A6: b |^ (ord b) = 1_ G by A4, GROUP_1:def 11;
a |^ (ord a) = b |^ (ord a) by A1, GROUP_4:1;
then A7: ord b divides ord a by A5, A6, GROUP_1:44, GROUP_2:44;
a |^ (ord b) = 1_ G by A1, A6, GROUP_4:1;
then a |^ (ord b) = 1_ H by GROUP_2:44;
then ord a divides ord b by GROUP_1:44;
hence ord a = ord b by A7, NAT_D:5; :: thesis: verum