let F be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for x being Element of F holds (0. F) * x = 0. F
let x be Element of F; :: thesis: (0. F) * x = 0. F
((0. F) * x) + (0. F) = (((0. F) + (0. F)) * x) + (0. F) by RLVECT_1:10
.= ((0. F) + (0. F)) * x by RLVECT_1:10
.= ((0. F) * x) + ((0. F) * x) by VECTSP_1:def 12 ;
hence (0. F) * x = 0. F by RLVECT_1:21; :: thesis: verum