let G be addGroup; :: thesis: for h being Element of G holds 1 * h = h
let h be Element of G; :: thesis: 1 * h = h
thus 1 * h = (0 + 1) * h
.= (0 * h) + h by Def7
.= (0_ G) + h by Def7
.= h by Def4 ; :: thesis: verum