let A be Universal_Algebra; :: thesis: for B being Subset of A ex C being Subset of A st
( C = union { (B |^ n) where n is Element of NAT : verum } & C is opers_closed )
let B be Subset of A; :: thesis: ex C being Subset of A st
( C = union { (B |^ n) where n is Element of NAT : verum } & C is opers_closed )
set X = { (B |^ n) where n is Element of NAT : verum } ;
set C = union { (B |^ n) where n is Element of NAT : verum } ;
A1: union (bool the carrier of A) = the carrier of A by ZFMISC_1:99;
{ (B |^ n) where n is Element of NAT : verum } c= bool the carrier of A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( x nin { (B |^ n) where n is Element of NAT : verum } or not x nin bool the carrier of A )
assume x in { (B |^ n) where n is Element of NAT : verum } ; :: thesis: not x nin bool the carrier of A
then ex n being Element of NAT st x = B |^ n ;
hence not x nin bool the carrier of A ; :: thesis: verum

end;

then reconsider C = union { (B |^ n) where n is Element of NAT : verum } as Subset of A by A1, ZFMISC_1:95;
take C ; :: thesis: ( C = union { (B |^ n) where n is Element of NAT : verum } & C is opers_closed )
thus C = union { (B |^ n) where n is Element of NAT : verum } ; :: thesis: C is opers_closed
let o be Element of Operations A; :: according to UNIALG_2:def 5 :: thesis: C is_closed_on o
consider s being set such that
A2: s in dom the charact of A and
A3: o = the charact of A . s by FUNCT_1:def 5;
reconsider s = s as OperSymbol of A by A2;
A4: dom o = (arity o) -tuples_on the carrier of A by MARGREL1:58;
let p be FinSequence of C; :: according to UNIALG_2:def 4 :: thesis: ( not len p = arity o or not o . p nin C )
assume len p = arity o ; :: thesis: not o . p nin C
then p is Element of dom (Den s,A) by A3, A4, FINSEQ_2:110;
then A5: p in dom (Den s,A) by A3, A4;
defpred S₁[ set , Nat] means $1 in B |^ $2;
A6: rng p is finite ;
A7: for x being Element of A st x in rng p holds
ex n being Nat st S₁[x,n]

proof

let x be Element of A; :: thesis: ( x in rng p implies ex n being Nat st S₁[x,n] )
assume A8: x in rng p ; :: thesis: ex n being Nat st S₁[x,n]
rng p c= C by FINSEQ_1:def 4;
then consider Y being set such that
A9: x in Y and
A10: Y in { (B |^ n) where n is Element of NAT : verum } by A8, TARSKI:def 4;
consider n being Element of NAT such that
A11: Y = B |^ n by A10;
take n ; :: thesis: S₁[x,n]
thus S₁[x,n] by A9, A11; :: thesis: verum

end;

A12: for x being Element of A
for n, m being Nat st S₁[x,n] & n <= m holds
S₁[x,m]

proof

let x be Element of A; :: thesis: for n, m being Nat st S₁[x,n] & n <= m holds
S₁[x,m]
let n, m be Nat; :: thesis: ( S₁[x,n] & n <= m implies S₁[x,m] )
assume A13: S₁[x,n] ; :: thesis: ( not n <= m or S₁[x,m] )
assume n <= m ; :: thesis: S₁[x,m]
then B |^ n c= B |^ m by Th21;
hence S₁[x,m] by A13; :: thesis: verum

end;

consider n being Nat such that
A14: for x being Element of A st x in rng p holds
S₁[x,n] from AOFA_000:sch 1(A6, A7, A12);
rng p c= B |^ n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( x nin rng p or not x nin B |^ n )
assume x in rng p ; :: thesis: not x nin B |^ n
hence not x nin B |^ n by A14; :: thesis: verum

end;

then (Den s,A) . p in { ((Den a,A) . r) where a is Element of dom the charact of A, r is Element of the carrier of A * : ( r in dom (Den a,A) & rng r c= B |^ n ) } by A5;
then ( o . p in (B |^ n) \/ { ((Den a,A) . r) where a is Element of dom the charact of A, r is Element of the carrier of A * : ( r in dom (Den a,A) & rng r c= B |^ n ) } & n + 1 in NAT ) by A3, XBOOLE_0:def 3;
then A15: o . p in B |^ (n + 1) by Th19;
B |^ (n + 1) in { (B |^ n) where n is Element of NAT : verum } ;
hence not o . p nin C by A15, TARSKI:def 4; :: thesis: verum