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