let G be Group; :: thesis: for h being Element of G holds h |^ (ord h) = 1_ G
let h be Element of G; :: thesis: h |^ (ord h) = 1_ G

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

suppose h is being_of_order_0 ; :: thesis: h |^ (ord h) = 1_ G

then ord h = 0 by Def11;
hence h |^ (ord h) = 1_ G by Def7; :: thesis: verum

end;

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

hence h |^ (ord h) = 1_ G by Def11; :: thesis: verum

end;

end;