theorem :: POLYNOM7:21

for X being set
for L being non empty ZeroStr
for a, b being Element of L holds
( a | (X,L) = b | (X,L) iff a = b )