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

now

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

end;

hence (0. L) * p = 0_. L by Def3; :: thesis: verum