let L be non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr ; :: thesis: for z0, z1, x being Element of L holds eval <%z0,(0. L)%>,x = z0
let z0, z1, x be Element of L; :: thesis: eval <%z0,(0. L)%>,x = z0
thus eval <%z0,(0. L)%>,x = z0 + ((0. L) * x) by Th45
.= z0 + (0. L) by VECTSP_1:39
.= z0 by RLVECT_1:def 7 ; :: thesis: verum