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

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 )
;

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;(1_ G) |^ m = 1_ G by GROUP_1:31;

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