let L be non empty right_zeroed addLoopStr ; :: thesis: for a being Element of L holds 2 * a = a + a
let a be Element of L; :: thesis: 2 * a = a + a
(Nat-mult-left L) . ((0 + 1),a) = a + ((Nat-mult-left L) . (0,a)) by BINOM:def 3
.= a + (0. L) by BINOM:def 3
.= a by RLVECT_1:def 4 ;
hence a + a = (Nat-mult-left L) . ((1 + 1),a) by BINOM:def 3
.= 2 * a ;
:: thesis: verum