let g be Element of G; :: thesis: ( g = n * h iff g = (mult G) . (n,h) )
|.n.| = n by ABSVALUE:def 1;
hence ( g = n * h iff g = (mult G) . (n,h) ) by Def8; :: thesis: verum