let F be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for x being Element of F holds x * (0. F) = 0. F
let x be Element of F; :: thesis: x * (0. F) = 0. F
(x * (0. F)) + (0. F) = (x * ((0. F) + (0. F))) + (0. F) by RLVECT_1:4
.= x * ((0. F) + (0. F)) by RLVECT_1:4
.= (x * (0. F)) + (x * (0. F)) by Def2 ;
hence x * (0. F) = 0. F by RLVECT_1:8; :: thesis: verum