let A be Universal_Algebra; :: thesis: for G being GeneratorSet of A
for a being Element of A st ( for o being Element of Operations A holds not a in rng o ) holds
a in G
let G be GeneratorSet of A; :: thesis: for a being Element of A st ( for o being Element of Operations A holds not a in rng o ) holds
a in G
let a be Element of A; :: thesis: ( ( for o being Element of Operations A holds not a in rng o ) implies a in G )
assume A1: for o being Element of Operations A holds a nin rng o ; :: thesis: a in G
defpred S₁[ Nat] means a nin G |^ $1;
assume a nin G ; :: thesis: contradiction
then A2: S₁[ 0 ] by Th18;

A3: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

assume a in G |^ (n + 1) ; :: thesis: contradiction
then a in (G |^ n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= G |^ n ) } by Th19;
then a in { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= G |^ n ) } by A4, XBOOLE_0:def 3;
then consider o being Element of dom the charact of A, p being Element of the carrier of A * such that
A5: a = (Den (o,A)) . p and
A6: p in dom (Den (o,A)) and
rng p c= G |^ n ;
a in rng (Den (o,A)) by A5, A6, FUNCT_1:def 3;
hence contradiction by A1; :: thesis: verum

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence contradiction by Th30; :: thesis: verum