let A be 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
let G be 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 o be OperSymbol of A; ( ( 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
; 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; ( 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))
; for n being Nat st (Den (o,A)) . p in G |^ (n + 1) holds
rng p c= G |^ n
let n be Nat; ( (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
; contradiction
reconsider p = p as FinSequence of A by A2, FINSEQ_1:def 11;
defpred S1[ 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 S1[n]
by A2, A3, A4;
consider n being Nat such that
A6:
( S1[n] & ( for m being Nat st S1[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;
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; verum