let G be Group; :: thesis: for g, h being Element of G ex f being Element of G st g * f = h
let g, h be Element of G; :: thesis: ex f being Element of G st g * f = h
take (g ") * h ; :: thesis: g * ((g ") * h) = h
thus g * ((g ") * h) = h by Th12; :: thesis: verum