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