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