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:4
.= ((0. F) + (0. F)) * x by RLVECT_1:4
.= ((0. F) * x) + ((0. F) * x) by Def3 ;
hence (0. F) * x = 0. F by RLVECT_1:8; :: thesis: verum