let G be Group; :: thesis: for f, h, g being Element of G holds
( f * h = g iff f = g * (h " ) )
let f, h, g be Element of G; :: thesis: ( f * h = g iff f = g * (h " ) )
(g * (h " )) * h = g * ((h " ) * h) by Def4
.= g * (1_ G) by Def6
.= g by Def5 ;
hence ( f * h = g implies f = g * (h " ) ) by Th14; :: thesis: ( f = g * (h " ) implies f * h = g )
assume f = g * (h " ) ; :: thesis: f * h = g
hence f * h = g * ((h " ) * h) by Def4
.= g * (1_ G) by Def6
.= g by Def5 ;
:: thesis: verum