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 a being set st a in rng p holds
a <> (Den o,A) . p
let o be OperSymbol of A; :: thesis: for p being FinSequence st p in dom (Den o,A) holds
for a being set st a in rng p holds
a <> (Den o,A) . p
let p be FinSequence; :: thesis: ( p in dom (Den o,A) implies for a being set st a in rng p holds
a <> (Den o,A) . p )
assume A1: p in dom (Den o,A) ; :: thesis: for a being set st a in rng p holds
a <> (Den o,A) . p
let a be set ; :: thesis: ( a in rng p implies a <> (Den o,A) . p )
assume A2: ( a in rng p & a = (Den o,A) . p ) ; :: thesis: contradiction
reconsider p = p as FinSequence of A by A1, FINSEQ_1:def 11;
a in rng p by A2;
then reconsider a = a as Element of A ;
set G = Generators A;
consider n being Nat such that
A3: a in (Generators A) |^ n by Th30;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Nat] means ex a being Element of A ex o being OperSymbol of A ex p being FinSequence of A st
( p in dom (Den o,A) & a in rng p & a = (Den o,A) . p & a in (Generators A) |^ $1 );
( a in rng p & a in (Generators A) |^ n ) by A2, A3;
then A4: ex n being Nat st S₁[n] by A1, A2;
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 a being Element of A, o being OperSymbol of A, p being FinSequence of A such that
A6: ( p in dom (Den o,A) & a in rng p & a = (Den o,A) . p & a in (Generators A) |^ n ) by A5;
reconsider op = Den o,A as Element of Operations A ;
a in rng op by A6, FUNCT_1:12;
then a nin Generators A by Th26;
then n <> 0 by A6, Th18;
then consider k being Nat such that
A7: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A8: k < n by A7, NAT_1:13;
then a nin (Generators A) |^ k by A5, A6;
then consider o' being Element of dom the charact of A, p' being Element of the carrier of A * such that
A9: ( a = (Den o',A) . p' & p' in dom (Den o',A) & rng p' c= (Generators A) |^ k ) by A6, A7, Th20;
p' = p by A6, A9, Th36;
hence contradiction by A5, A6, A9, A8; :: thesis: verum