let A be Universal_Algebra; 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; 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; ( ( 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
; a in G
defpred S1[ Nat] means a nin G |^ $1;
assume
a nin G
; contradiction
then A2:
S1[ 0 ]
by Th18;
A3:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A4:
S1[
n]
;
S1[n + 1]thus
S1[
n + 1]
verumproof
assume
a in G |^ (n + 1)
;
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;
verum
end; end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A3);
hence
contradiction
by Th30; verum