let G be Group; :: thesis: for h being Element of holds h |^ (ord h) = 1_ G
let h be Element of ; :: 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 Def12;
hence h |^ (ord h) = 1_ G by Def8; :: thesis: verum

end;

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

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

end;

end;