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

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