for X being set
for L being non empty ZeroStr holds (0. L) | (X,L) = 0_ (X,L) by Lm3;