let R be Ring; :: thesis: for a being Element of R holds 2 '*' a = a + a
let a be Element of R; :: thesis: 2 '*' a = a + a
thus 2 '*' a = (1 + 1) '*' a
.= (1 '*' a) + (1 '*' a) by RING_3:62
.= a + (1 '*' a) by RING_3:60
.= a + a by RING_3:60 ; :: thesis: verum