let A be free Universal_Algebra; :: thesis: for G being GeneratorSet of A
for o being OperSymbol of A st ( for o' being OperSymbol of A
for p being FinSequence st p in dom (Den o',A) & (Den o',A) . p in G holds
o' <> 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
let G be GeneratorSet of A; :: thesis: for o being OperSymbol of A st ( for o' being OperSymbol of A
for p being FinSequence st p in dom (Den o',A) & (Den o',A) . p in G holds
o' <> 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
let o be OperSymbol of A; :: thesis: ( ( for o' being OperSymbol of A
for p being FinSequence st p in dom (Den o',A) & (Den o',A) . p in G holds
o' <> o ) implies 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 )
assume A1: for o' being OperSymbol of A
for p being FinSequence st p in dom (Den o',A) & (Den o',A) . p in G holds
o' <> o ; :: thesis: 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
let p be FinSequence; :: thesis: ( p in dom (Den o,A) implies for n being Nat st (Den o,A) . p in G |^ (n + 1) holds
rng p c= G |^ n )
assume A2: p in dom (Den o,A) ; :: thesis: for n being Nat st (Den o,A) . p in G |^ (n + 1) holds
rng p c= G |^ n
let n be Nat; :: thesis: ( (Den o,A) . p in G |^ (n + 1) implies rng p c= G |^ n )
assume A3: ( (Den o,A) . p in G |^ (n + 1) & not rng p c= G |^ n ) ; :: thesis: contradiction
reconsider p = p as FinSequence of A by A2, FINSEQ_1:def 11;
defpred S₁[ Nat] means ex p being FinSequence of A st
( p in dom (Den o,A) & (Den o,A) . p in G |^ ($1 + 1) & not rng p c= G |^ $1 );
( p is FinSequence of A & n is Element of NAT ) by ORDINAL1:def 13;
then A4: ex n being Nat st S₁[n] by A2, A3;
consider n being Nat such that
A5: ( S₁[n] & ( for m being Nat st S₁[m] holds
n <= m ) ) from NAT_1:sch 5(A4);
consider p being FinSequence of A such that
A6: ( p in dom (Den o,A) & (Den o,A) . p in G |^ (n + 1) & not rng p c= G |^ n ) by A5;
set a = (Den o,A) . p;

now

assume A7: (Den o,A) . p in G |^ n ; :: thesis: contradiction
(Den o,A) . p nin G by A1, A6;
then n <> 0 by A7, Th18;
then consider k being Nat such that
A8: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A9: k < n by A8, NAT_1:13;
then G |^ k c= G |^ n by Th21;
then not rng p c= G |^ k by A6, XBOOLE_1:1;
hence contradiction by A5, A6, A7, A8, A9; :: thesis: verum

end;

then ex o' being Element of dom the charact of A ex p' being Element of the carrier of A * st
( (Den o,A) . p = (Den o',A) . p' & p' in dom (Den o',A) & rng p' c= G |^ n ) by A6, Th20;
hence contradiction by A6, Th36; :: thesis: verum