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,(1. L)%>,x) = z0 + x
let z0, z1, x be Element of L; :: thesis: eval (<%z0,(1. L)%>,x) = z0 + x
thus eval (<%z0,(1. L)%>,x) = z0 + ((1. L) * x) by Th44
.= z0 + x ; :: thesis: verum