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