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