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

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