theorem :: POLYNOM7:20

for X being set
for L being non empty well-unital multLoopStr_0 holds (1. L) | (X,L) = 1_ (X,L)