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 object ; :: 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 ;
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 object ; :: 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 object ; :: 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 }

let r, s be object ; :: according to RELAT_1:def 2 :: thesis:
thus ( [r,s] in g | (fs \ {n}) implies [r,s] in g \ { [n,x] where x is Element of V : x in a } ) :: thesis:

assume A28: [r,s] in g | (fs \ {n}) ; :: thesis:
r in fs \ {n} by A26, A28, FUNCT_1:1;
then not r in {n} by XBOOLE_0:def 5;
then A29: r <> n by TARSKI:def 1;
A30: 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 A29, XTUPLE_0:1; :: thesis:

end;

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

end;

assume A31: [r,s] in g \ { [n,x] where x is Element of V : x in a } ; :: thesis:
A32: s = g . r by A31, FUNCT_1:1;
A33: r in dom g by A31, FUNCT_1:1;
then A34: s in rng g by A32, FUNCT_1:def 3;
n <> r

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

end;

then not r in {n} by TARSKI:def 1;
then A35: r in fs \ {n} by A24, A33, XBOOLE_0:def 5;
then s = (g | (fs \ {n})) . r by A32, FUNCT_1:49;
hence [r,s] in g | (fs \ {n}) by A26, A35, 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;
then A36: 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 A36, 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 r, s be object ; :: according to RELAT_1:def 3 :: thesis:
A37: 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;
A38: [n,a1] in { [n,x] where x is Element of V : x in a } by A25, A37;
set p = [r,s];
assume [r,s] in {[n,(g . n)]} ; :: thesis:
then A39: [r,s] = [n,(g . n)] by TARSKI:def 1;
then [r,s] in y by A2, A23, A24, FUNCT_1:1;
hence [r,s] in y /\ { [n,x] where x is Element of V : x in a } by A39, A38, XBOOLE_0:def 4; :: thesis:

end;

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A40: 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 A41: ex x being Element of V st
( p = [n,x] & x in a ) ;
p in y by A40, XBOOLE_0:def 4;
then p = [n,(g . n)] by A23, A41, 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, A36;
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 object ; :: 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
A42: q = x and
A43: x in Funcs ((fs \ {n}),a) and
A44: ex u being set st {[n,u]} \/ x in b ;
consider u being set such that
A45: {[n,u]} \/ x in b by A44;
reconsider y = {[n,u]} \/ x as Element of V by A4, A45, Th1;
A46: x = y \ z

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

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A49: p in x ; :: thesis:
then consider a1, a2 being object such that
A50: p = [a1,a2] by A47, RELAT_1:def 1;
a1 in dom g by A47, A49, A50, FUNCT_1:1;
then A51: not a1 in {n} by A48, XBOOLE_0:def 5;
A52: 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 A50, XTUPLE_0:1;
hence contradiction by A51, TARSKI:def 1; :: thesis:

end;

p in y by A49, XBOOLE_0:def 3;
hence p in y \ z by A52, XBOOLE_0:def 5; :: thesis:

end;

thus y \ z c= x :: thesis:

A53: x misses z

assume not x misses z ; :: thesis:
then consider r being object such that
A54: r in g and
A55: r in z by A47, XBOOLE_0:3;
consider a1, a2 being object such that
A56: r = [a1,a2] by A54, RELAT_1:def 1;
a1 in dom g by A54, A56, FUNCT_1:1;
then A57: not a1 in {n} by A48, 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 A56, XTUPLE_0:1;
hence contradiction by A57, TARSKI:def 1; :: thesis:

end;

hence contradiction by A55; :: thesis:

end;

{[n,u]} c= z

consider g being Function such that
A58: {[n,u]} \/ x = g and
dom g = fs and
A59: rng g c= a by A5, A45, FUNCT_2:def 2;
{[n,u]} c= g by A58, 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 A60: u in rng g by FUNCT_1:def 3;
then reconsider a1 = u as Element of V by A3, A59, Th1;
assume not {[n,u]} c= z ; :: thesis:
then A61: ex r being object st
( r in {[n,u]} & not r in z ) ;
[n,a1] in z by A59, A60;
hence contradiction by A61, TARSKI:def 1; :: thesis:

end;

then {[n,u]} \ z = {} by XBOOLE_1:37;
then A62: (x \ z) \/ ({[n,u]} \ z) = x by A53, XBOOLE_1:83;
let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in y \ z ; :: thesis:
hence p in x by A62, 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 A42, A45, A46; :: thesis:

end;

X is closed_wrt_A6 by A1;
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; :: thesis: