let G be addGroup; :: 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