theorem Th38: :: AOFA_000:38

for A being free Universal_Algebra
for o being OperSymbol of A
for p being FinSequence st p in dom (Den (o,A)) holds
for a being set st a in rng p holds
a <> (Den (o,A)) . p