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 that
A2: a in rng p and
A3: 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
A4: a in (Generators A) |^ n by Th30;
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 by A2;
then A5: ex n being Nat st S₁[n] by A1, 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 a being Element of A, o being OperSymbol of A, p being FinSequence of A such that
A7: p in dom (Den (o,A)) and
A8: a in rng p and
A9: a = (Den (o,A)) . p and
A10: a in (Generators A) |^ n by A6;
reconsider op = Den (o,A) as Element of Operations A ;
a in rng op by A7, A9, FUNCT_1:3;
then a nin Generators A by Th26;
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 a nin (Generators A) |^ k by A6, A7, A8, A9;
then consider o9 being Element of dom the charact of A, p9 being Element of the carrier of A * such that
A13: a = (Den (o9,A)) . p9 and
A14: p9 in dom (Den (o9,A)) and
A15: rng p9 c= (Generators A) |^ k by A10, A11, Th20;
p9 = p by A7, A9, A13, A14, Th36;
hence contradiction by A6, A7, A8, A9, A12, A15; :: thesis: verum