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 Th22; :: thesis: verum