let A be free Universal_Algebra; :: thesis: for o being OperSymbol of A
for p being FinSequence st p in dom (Den o,A) holds
for n being Nat st (Den o,A) . p in (Generators A) |^ (n + 1) holds
rng p c= (Generators A) |^ n
set G = Generators A;
let o be OperSymbol of A; :: thesis: for p being FinSequence st p in dom (Den o,A) holds
for n being Nat st (Den o,A) . p in (Generators A) |^ (n + 1) holds
rng p c= (Generators A) |^ n

now

let o9 be OperSymbol of A; :: thesis: for p being FinSequence st p in dom (Den o9,A) & (Den o9,A) . p in Generators A holds
o9 <> o
let p be FinSequence; :: thesis: ( p in dom (Den o9,A) & (Den o9,A) . p in Generators A implies o9 <> o )
reconsider op = Den o9,A as Element of Operations A ;
assume p in dom (Den o9,A) ; :: thesis: ( (Den o9,A) . p in Generators A implies o9 <> o )
then op . p in rng op by FUNCT_1:12;
hence ( (Den o9,A) . p in Generators A implies o9 <> o ) by Th26; :: thesis: verum

end;

hence for p being FinSequence st p in dom (Den o,A) holds
for n being Nat st (Den o,A) . p in (Generators A) |^ (n + 1) holds
rng p c= (Generators A) |^ n by Th39; :: thesis: verum