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