let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for v being Element of L holds v * (0_. L) = 0_. L
let v be Element of L; :: thesis: v * (0_. L) = 0_. L

now :: thesis: for n being Element of NAT holds (0_. L) . n = v * ((0_. L) . n)

let n be Element of NAT ; :: thesis: (0_. L) . n = v * ((0_. L) . n)
thus (0_. L) . n = 0. L by FUNCOP_1:7
.= v * (0. L)
.= v * ((0_. L) . n) by FUNCOP_1:7 ; :: thesis: verum

end;

hence v * (0_. L) = 0_. L by Def4; :: thesis: verum