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