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