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