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