theorem Th39: :: AOFA_000:39

for A being free Universal_Algebra
for G being GeneratorSet of A
for o being OperSymbol of A st ( for o9 being OperSymbol of A
for p being FinSequence st p in dom (Den (o9,A)) & (Den (o9,A)) . p in G holds
o9 <> o ) holds
for p being FinSequence st p in dom (Den (o,A)) holds
for n being Nat st (Den (o,A)) . p in G |^ (n + 1) holds
rng p c= G |^ n