let V be Universe; :: thesis:
let a, b be Element of V; :: thesis:
let X be Subclass of V; :: thesis:
let n be Element of omega ; :: thesis:
let fs be finite Subset of omega; :: thesis:
assume that
A1: X is closed_wrt_A1-A7 and
A2: n in fs and
A3: a in X and
A4: b in X and
A5: b c= Funcs (fs,a) ; :: thesis:
A6: Funcs ({n},a) in X by A1, A3, Th9;
then reconsider F = Funcs ({n},a) as Element of V ;
set T = { [n,x] where x is Element of V : x in a } ;
A7: { [n,x] where x is Element of V : x in a } = union F

thus { [n,x] where x is Element of V : x in a } c= union F :: according to XBOOLE_0:def 10 :: thesis:

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume q in { [n,x] where x is Element of V : x in a } ; :: thesis:
then consider x being Element of V such that
A8: q = [n,x] and
A9: x in a ;
reconsider g = {[n,x]} as Function by GRFUNC_1:5;
rng g = {x} by RELAT_1:9;
then ( dom g = {n} & rng g c= a ) by A9, RELAT_1:9, ZFMISC_1:31;
then A10: g in F by FUNCT_2:def 2;
q in g by A8, TARSKI:def 1;
hence q in union F by A10, TARSKI:def 4; :: thesis:

end;

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume q in union F ; :: thesis:
then consider A being set such that
A11: q in A and
A12: A in F by TARSKI:def 4;
consider g being Function such that
A13: A = g and
A14: dom g = {n} and
A15: rng g c= a by A12, FUNCT_2:def 2;
n in dom g by A14, TARSKI:def 1;
then A16: g . n in rng g by FUNCT_1:def 3;
then reconsider o = g . n as Element of V by A3, A15, Th1;
q in {[n,(g . n)]} by A11, A13, A14, GRFUNC_1:7;
then q = [n,o] by TARSKI:def 1;
hence q in { [n,x] where x is Element of V : x in a } by A15, A16; :: thesis:

end;

then { [n,x] where x is Element of V : x in a } in X by A1, A6, Th2;
then A17: { { [n,x] where x is Element of V : x in a } } in X by A1, Th2;
then reconsider t = { { [n,x] where x is Element of V : x in a } } as Element of V ;
set Y = { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } ;
set Z = { (y \ z) where y, z is Element of V : ( y in b & z in t ) } ;
A18: { (y \ z) where y, z is Element of V : ( y in b & z in t ) } = { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) }

thus { (y \ z) where y, z is Element of V : ( y in b & z in t ) } c= { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } :: according to XBOOLE_0:def 10 :: thesis:

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume q in { (y \ z) where y, z is Element of V : ( y in b & z in t ) } ; :: thesis:
then consider y, z being Element of V such that
A19: q = y \ z and
A20: y in b and
A21: z in t ;
A22: q = y \ { [n,x] where x is Element of V : x in a } by A19, A21, TARSKI:def 1;
consider g being Function such that
A23: y = g and
A24: dom g = fs and
A25: rng g c= a by A5, A20, FUNCT_2:def 2;
set h = g | (fs \ {n});
A26: dom (g | (fs \ {n})) = fs /\ (fs \ {n}) by A24, RELAT_1:61
.= (fs /\ fs) \ (fs /\ {n}) by XBOOLE_1:50
.= fs \ {n} by XBOOLE_1:47 ;
A27: g | (fs \ {n}) = g \ { [n,x] where x is Element of V : x in a }

thus g | (fs \ {n}) c= g \ { [n,x] where x is Element of V : x in a } :: according to XBOOLE_0:def 10 :: thesis:

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: p in g | (fs \ {n}) ; :: thesis:
then consider r, s being set such that
A29: p = [r,s] by RELAT_1:def 1;
r in fs \ {n} by A26, A28, A29, FUNCT_1:1;
then not r in {n} by XBOOLE_0:def 5;
then A30: r <> n by TARSKI:def 1;
A31: not [r,s] in { [n,x] where x is Element of V : x in a }

assume [r,s] in { [n,x] where x is Element of V : x in a } ; :: thesis:
then ex x being Element of V st
( [r,s] = [n,x] & x in a ) ;
hence contradiction by A30, ZFMISC_1:27; :: thesis:

end;

[r,s] in g by A28, A29, RELAT_1:def 11;
hence p in g \ { [n,x] where x is Element of V : x in a } by A29, A31, XBOOLE_0:def 5; :: thesis:

end;

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A32: p in g \ { [n,x] where x is Element of V : x in a } ; :: thesis:
then consider r, s being set such that
A33: p = [r,s] by RELAT_1:def 1;
A34: s = g . r by A32, A33, FUNCT_1:1;
A35: r in dom g by A32, A33, FUNCT_1:1;
then A36: s in rng g by A34, FUNCT_1:def 3;
n <> r

reconsider a1 = s as Element of V by A3, A25, A36, Th1;
assume n = r ; :: thesis:
then [r,a1] in { [n,x] where x is Element of V : x in a } by A25, A36;
hence contradiction by A32, A33, XBOOLE_0:def 5; :: thesis:

end;

then not r in {n} by TARSKI:def 1;
then A37: r in fs \ {n} by A24, A35, XBOOLE_0:def 5;
then s = (g | (fs \ {n})) . r by A34, FUNCT_1:49;
hence p in g | (fs \ {n}) by A26, A33, A37, FUNCT_1:1; :: thesis:

end;

rng (g | (fs \ {n})) c= rng g by RELAT_1:70;
then rng (g | (fs \ {n})) c= a by A25, XBOOLE_1:1;
then A38: q in Funcs ((fs \ {n}),a) by A22, A23, A26, A27, FUNCT_2:def 2;
Funcs ((fs \ {n}),a) in X by A1, A3, Th9;
then reconsider a2 = q as Element of V by A38, Th1;
{[n,(g . n)]} = y /\ { [n,x] where x is Element of V : x in a }

thus {[n,(g . n)]} c= y /\ { [n,x] where x is Element of V : x in a } :: according to XBOOLE_0:def 10 :: thesis:

let p be set ; :: according to TARSKI:def 3 :: thesis:
A39: g . n in rng g by A2, A24, FUNCT_1:def 3;
then reconsider a1 = g . n as Element of V by A3, A25, Th1;
A40: [n,a1] in { [n,x] where x is Element of V : x in a } by A25, A39;
assume p in {[n,(g . n)]} ; :: thesis:
then A41: p = [n,(g . n)] by TARSKI:def 1;
then p in y by A2, A23, A24, FUNCT_1:1;
hence p in y /\ { [n,x] where x is Element of V : x in a } by A41, A40, XBOOLE_0:def 4; :: thesis:

end;

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A42: p in y /\ { [n,x] where x is Element of V : x in a } ; :: thesis:
then p in { [n,x] where x is Element of V : x in a } by XBOOLE_0:def 4;
then A43: ex x being Element of V st
( p = [n,x] & x in a ) ;
p in y by A42, XBOOLE_0:def 4;
then p = [n,(g . n)] by A23, A43, FUNCT_1:1;
hence p in {[n,(g . n)]} by TARSKI:def 1; :: thesis:

end;

then {[n,(g . n)]} \/ (y \ { [n,x] where x is Element of V : x in a } ) in b by A20, XBOOLE_1:51;
then a2 in { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } by A22, A38;
hence q in { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } ; :: thesis:

end;

reconsider z = { [n,x] where x is Element of V : x in a } as Element of V by A7;
let q be set ; :: according to TARSKI:def 3 :: thesis:
assume q in { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } ; :: thesis:
then consider x being Element of V such that
A44: q = x and
A45: x in Funcs ((fs \ {n}),a) and
A46: ex u being set st {[n,u]} \/ x in b ;
consider u being set such that
A47: {[n,u]} \/ x in b by A46;
reconsider y = {[n,u]} \/ x as Element of V by A4, A47, Th1;
A48: x = y \ z

consider g being Function such that
A49: x = g and
A50: dom g = fs \ {n} and
rng g c= a by A45, FUNCT_2:def 2;
thus x c= y \ z :: according to XBOOLE_0:def 10 :: thesis:

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A51: p in x ; :: thesis:
then consider a1, a2 being set such that
A52: p = [a1,a2] by A49, RELAT_1:def 1;
a1 in dom g by A49, A51, A52, FUNCT_1:1;
then A53: not a1 in {n} by A50, XBOOLE_0:def 5;
A54: not p in z

assume p in z ; :: thesis:
then ex x9 being Element of V st
( p = [n,x9] & x9 in a ) ;
then a1 = n by A52, ZFMISC_1:27;
hence contradiction by A53, TARSKI:def 1; :: thesis:

end;

p in y by A51, XBOOLE_0:def 3;
hence p in y \ z by A54, XBOOLE_0:def 5; :: thesis:

end;

thus y \ z c= x :: thesis:

A55: x misses z

assume not x misses z ; :: thesis:
then consider r being set such that
A56: r in g and
A57: r in z by A49, XBOOLE_0:3;
consider a1, a2 being set such that
A58: r = [a1,a2] by A56, RELAT_1:def 1;
a1 in dom g by A56, A58, FUNCT_1:1;
then A59: not a1 in {n} by A50, XBOOLE_0:def 5;
not r in z

assume r in z ; :: thesis:
then ex x9 being Element of V st
( r = [n,x9] & x9 in a ) ;
then a1 = n by A58, ZFMISC_1:27;
hence contradiction by A59, TARSKI:def 1; :: thesis:

end;

hence contradiction by A57; :: thesis:

end;

{[n,u]} c= z

consider g being Function such that
A60: {[n,u]} \/ x = g and
dom g = fs and
A61: rng g c= a by A5, A47, FUNCT_2:def 2;
{[n,u]} c= g by A60, XBOOLE_1:7;
then [n,u] in g by ZFMISC_1:31;
then ( n in dom g & u = g . n ) by FUNCT_1:1;
then A62: u in rng g by FUNCT_1:def 3;
then reconsider a1 = u as Element of V by A3, A61, Th1;
assume not {[n,u]} c= z ; :: thesis:
then A63: ex r being set st
( r in {[n,u]} & not r in z ) by TARSKI:def 3;
[n,a1] in z by A61, A62;
hence contradiction by A63, TARSKI:def 1; :: thesis:

end;

then {[n,u]} \ z = {} by XBOOLE_1:37;
then A64: (x \ z) \/ ({[n,u]} \ z) = x by A55, XBOOLE_1:83;
let p be set ; :: according to TARSKI:def 3 :: thesis:
assume p in y \ z ; :: thesis:
hence p in x by A64, XBOOLE_1:42; :: thesis:

end;

end;

z in t by TARSKI:def 1;
hence q in { (y \ z) where y, z is Element of V : ( y in b & z in t ) } by A44, A47, A48; :: thesis:

end;

X is closed_wrt_A6 by A1, Def13;
hence { x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X by A4, A17, A18, Def11; :: thesis: