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

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