let V be Universe; :: thesis: for a being Element of V
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs fs,a in X
let a be Element of V; :: thesis: for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs fs,a in X
let X be Subclass of V; :: thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs fs,a in X
let fs be finite Subset of omega ; :: thesis: ( X is closed_wrt_A1-A7 & a in X implies Funcs fs,a in X )
defpred S₁[ set ] means Funcs $1,a in X;
assume A1: ( X is closed_wrt_A1-A7 & a in X ) ; :: thesis: Funcs fs,a in X
then A2: X is closed_wrt_A5 by Def13;
A3: X is closed_wrt_A4 by A1, Def13;
A4: fs is finite ;
A5: S₁[ {} ]

proof

A6: Funcs {} ,a = {{} } by FUNCT_5:64;
{} in X by A1, Th3;
hence S₁[ {} ] by A1, A6, Th2; :: thesis: verum

end;

A7: for o, B being set st o in fs & B c= fs & S₁[B] holds
S₁[B \/ {o}]

proof

let o, B be set ; :: thesis: ( o in fs & B c= fs & S₁[B] implies S₁[B \/ {o}] )
assume A8: ( o in fs & B c= fs & Funcs B,a in X ) ; :: thesis: S₁[B \/ {o}]

per cases ( B meets {o} or B misses {o} ) ;

suppose B meets {o} ; :: thesis: S₁[B \/ {o}]

hence S₁[B \/ {o}] by A8, ZFMISC_1:46, ZFMISC_1:56; :: thesis: verum

end;

suppose A9: B misses {o} ; :: thesis: S₁[B \/ {o}]

A10: omega c= X by A1, Th7;
A11: o in omega by A8;
then A12: o in X by A10;
A13: {o} in X by A1, A10, A11, Th2;
set r = {o};
reconsider p = o as Element of V by A12;
set A = { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } ;
Funcs {o},a = { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) }

proof

thus Funcs {o},a c= { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } :: according to XBOOLE_0:def 10 :: thesis: { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } c= Funcs {o},a

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in Funcs {o},a or q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } )
assume q in Funcs {o},a ; :: thesis: q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) }
then consider g being Function such that
A14: ( q = g & dom g = {o} & rng g c= a ) by FUNCT_2:def 2;
o in dom g by A14, TARSKI:def 1;
then A15: g . o in rng g by FUNCT_1:def 5;
A16: o in {o} by TARSKI:def 1;
reconsider s = g . o as Element of V by A1, A14, A15, Th1;
g = {[p,s]} by A14, GRFUNC_1:18;
hence q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } by A14, A15, A16; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } or q in Funcs {o},a )
assume q in { {[x,y]} where x, y is Element of V : ( x in {o} & y in a ) } ; :: thesis: q in Funcs {o},a
then consider x, y being Element of V such that
A17: ( q = {[x,y]} & x in {o} & y in a ) ;
reconsider g = q as Function by A17, GRFUNC_1:15;
x = o by A17, TARSKI:def 1;
then A18: ( dom g = {o} & rng g = {y} ) by A17, RELAT_1:23;
then rng g c= a by A17, ZFMISC_1:37;
hence q in Funcs {o},a by A18, FUNCT_2:def 2; :: thesis: verum

end;

then A19: Funcs {o},a in X by A1, A3, A13, Def9;
reconsider x = Funcs B,a as Element of V by A8;
reconsider y = Funcs {o},a as Element of V by A19;
set Z = { (x' \/ y') where x', y' is Element of V : ( x' in x & y' in y ) } ;
Funcs (B \/ {o}),a = { (x' \/ y') where x', y' is Element of V : ( x' in x & y' in y ) }

proof

thus Funcs (B \/ {o}),a c= { (x' \/ y') where x', y' is Element of V : ( x' in x & y' in y ) } :: according to XBOOLE_0:def 10 :: thesis: { (x' \/ y') where x', y' is Element of V : ( x' in x & y' in y ) } c= Funcs (B \/ {o}),a

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in Funcs (B \/ {o}),a or q in { (x' \/ y') where x', y' is Element of V : ( x' in x & y' in y ) } )
assume q in Funcs (B \/ {o}),a ; :: thesis: q in { (x' \/ y') where x', y' is Element of V : ( x' in x & y' in y ) }
then consider g being Function such that
A20: ( q = g & dom g = B \/ {o} & rng g c= a ) by FUNCT_2:def 2;
set A = g | B;
set C = g | {o};
A21: dom (g | B) = (B \/ {o}) /\ B by A20, RELAT_1:90
.= B by XBOOLE_1:21 ;
rng (g | B) c= rng g by RELAT_1:99;
then rng (g | B) c= a by A20, XBOOLE_1:1;
then A22: g | B in x by A21, FUNCT_2:def 2;
then reconsider x' = g | B as Element of V by A8, Th1;
A23: dom (g | {o}) = (B \/ {o}) /\ {o} by A20, RELAT_1:90
.= {o} by XBOOLE_1:21 ;
rng (g | {o}) c= rng g by RELAT_1:99;
then rng (g | {o}) c= a by A20, XBOOLE_1:1;
then A24: g | {o} in y by A23, FUNCT_2:def 2;
then reconsider y' = g | {o} as Element of V by A19, Th1;
g = g | (B \/ {o}) by A20, RELAT_1:97
.= (g | B) \/ (g | {o}) by RELAT_1:107 ;
then q = x' \/ y' by A20;
hence q in { (x' \/ y') where x', y' is Element of V : ( x' in x & y' in y ) } by A22, A24; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (x' \/ y') where x', y' is Element of V : ( x' in x & y' in y ) } or q in Funcs (B \/ {o}),a )
assume q in { (x' \/ y') where x', y' is Element of V : ( x' in x & y' in y ) } ; :: thesis: q in Funcs (B \/ {o}),a
then consider x', y' being Element of V such that
A25: ( q = x' \/ y' & x' in x & y' in y ) ;
consider e being Function such that
A26: ( x' = e & dom e = B & rng e c= a ) by A25, FUNCT_2:def 2;
consider g being Function such that
A27: ( y' = g & dom g = {o} & rng g c= a ) by A25, FUNCT_2:def 2;
reconsider h = e \/ g as Function by A9, A26, A27, GRFUNC_1:31;
A28: dom h = B \/ {o} by A26, A27, RELAT_1:13;
rng h = (rng e) \/ (rng g) by RELAT_1:26;
then rng h c= a \/ a by A26, A27, XBOOLE_1:13;
hence q in Funcs (B \/ {o}),a by A25, A26, A27, A28, FUNCT_2:def 2; :: thesis: verum

end;

hence S₁[B \/ {o}] by A2, A8, A19, Def10; :: thesis: verum

end;

end;

end;

thus S₁[fs] from FINSET_1:sch 2(A4, A5, A7); :: thesis: verum