let E be RealNormSpace; :: thesis: for a being Point of E holds a + a = 2 * a
let a be Point of E; :: thesis: a + a = 2 * a
1 * a = a by RLVECT_1:def 8;
hence a + a = (1 + 1) * a by RLVECT_1:def 6
.= 2 * a ;
:: thesis: verum