theorem :: POLNOT_1:77

for L being non trivial Polish-language
for E being Polish-arity-function of L
for t, u being Element of L st rng (Polish-operation (L,E,t)) meets rng (Polish-operation (L,E,u)) holds
t = u