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
for n being Element of NAT holds (0_. L) . n = (0. L) * (p . n) by FUNCOP_1:7;
hence (0. L) * p = 0_. L by Def4; :: thesis: verum