let G be strict Group; :: thesis: for a being Element of G
for m being Integer holds a |^ (m * (ord a)) = 1_ G
let a be Element of G; :: thesis: for m being Integer holds a |^ (m * (ord a)) = 1_ G
let m be Integer; :: thesis: a |^ (m * (ord a)) = 1_ G

per cases ( a is being_of_order_0 or not a is being_of_order_0 ) ;

suppose a is being_of_order_0 ; :: thesis: a |^ (m * (ord a)) = 1_ G

then ord a = 0 by GROUP_1:def 11;
hence a |^ (m * (ord a)) = 1_ G by GROUP_1:25; :: thesis: verum

end;

suppose not a is being_of_order_0 ; :: thesis: a |^ (m * (ord a)) = 1_ G

then A1: a |^ (ord a) = 1_ G by GROUP_1:def 11;
(1_ G) |^ m = 1_ G by GROUP_1:31;
hence a |^ (m * (ord a)) = 1_ G by A1, GROUP_1:35; :: thesis: verum

end;

end;