let R be non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr ; :: thesis: for a being Element of R holds (0. R) * a = 0. R
let a be Element of R; :: thesis: (0. R) * a = 0. R
(0. R) * a = ((0. R) + (0. R)) * a by RLVECT_1:def 4
.= ((0. R) * a) + ((0. R) * a) by VECTSP_1:def 3 ;
then ((0. R) * a) + ((0. R) * a) = ((0. R) * a) + (0. R) by RLVECT_1:def 4;
hence (0. R) * a = 0. R by ALGSTR_0:def 3; :: thesis: verum