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 & o = the charact of A . s ) by FUNCT_1:def 5;
reconsider s = s as OperSymbol of A by A2;
A3: dom o = (arity o) -tuples_on the carrier of A by UNIALG_2:2;
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, A2, FINSEQ_2:110;
then A4: p in dom (Den s,A) by A3, A2;
defpred S₁[ set , Nat] means $1 in B |^ $2;
A5: rng p is finite ;
A6: 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 A7: 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
A8: ( x in Y & Y in { (B |^ n) where n is Element of NAT : verum } ) by A7, TARSKI:def 4;
consider n being Element of NAT such that
A9: Y = B |^ n by A8;
take n ; :: thesis: S₁[x,n]
thus S₁[x,n] by A8, A9; :: thesis: verum

end;

A10: 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 A11: 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 A11; :: thesis: verum

end;

consider n being Nat such that
A12: for x being Element of A st x in rng p holds
S₁[x,n] from AOFA_000:sch 1(A5, A6, A10);
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 A12; :: 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 A4;
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 A2, XBOOLE_0:def 3;
then ( o . p in B |^ (n + 1) & B |^ (n + 1) in { (B |^ n) where n is Element of NAT : verum } ) by Th19;
hence not o . p nin C by TARSKI:def 4; :: thesis: verum