let A be free Universal_Algebra; :: thesis: 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
let G be GeneratorSet of A; :: thesis: 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
let o be OperSymbol of A; :: thesis: ( ( 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 ) 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 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 ; :: 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 that
A3: (Den (o,A)) . p in G |^ (n + 1) and
A4: 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 ;
then A5: ex n being Nat st S₁[n] by A2, A3, A4;
consider n being Nat such that
A6: ( S₁[n] & ( for m being Nat st S₁[m] holds
n <= m ) ) from NAT_1:sch 5(A5);
consider p being FinSequence of A such that
A7: p in dom (Den (o,A)) and
A8: (Den (o,A)) . p in G |^ (n + 1) and
A9: not rng p c= G |^ n by A6;
set a = (Den (o,A)) . p;

now :: thesis: not (Den (o,A)) . p in G |^ n

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

end;

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