let R be non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr ; :: thesis: for a being Element of R holds a * (0. R) = 0. R
let a be Element of R; :: thesis: a * (0. R) = 0. R
a * (0. R) = a * ((0. R) + (0. R)) by ALGSTR_1:def 2
.= (a * (0. R)) + (a * (0. R)) by VECTSP_1:def 2 ;
then (a * (0. R)) + (a * (0. R)) = (0. R) + (a * (0. R)) by ALGSTR_1:def 2;
hence a * (0. R) = 0. R by ALGSTR_0:def 4; :: thesis: verum