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