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 :: thesis: for o9 being OperSymbol of A
for p being FinSequence st p in dom (Den (o9,A)) & (Den (o9,A)) . p in Generators A holds
o9 <> o
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:3;
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