let n be Ordinal; for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L)
let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L)
let p be Series of n,L; (0_ (n,L)) *' p = 0_ (n,L)
set Z = 0_ (n,L);
hence
(0_ (n,L)) *' p = 0_ (n,L)
by FUNCT_2:63; verum