let G be addGroup; :: thesis: for h being Element of G holds (ord h) * h = 0_ G
let h be Element of G; :: thesis: (ord h) * h = 0_ 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: (ord h) * h = 0_ G

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

end;

suppose not h is being_of_order_0 ; :: thesis: (ord h) * h = 0_ G

hence (ord h) * h = 0_ G by Def11; :: thesis: verum

end;

end;