let V be set ; :: thesis: for C being finite set
for A being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C)
for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds
ex b being finite set st
( b in - A & b c= a )
let C be finite set ; :: thesis: for A being Element of SubstitutionSet (V,C)
for a being Element of PFuncs (V,C)
for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds
ex b being finite set st
( b in - A & b c= a )
let A be Element of SubstitutionSet (V,C); :: thesis: for a being Element of PFuncs (V,C)
for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds
ex b being finite set st
( b in - A & b c= a )
let a be Element of PFuncs (V,C); :: thesis: for B being Element of SubstitutionSet (V,C) st B = {a} & A ^ B = {} holds
ex b being finite set st
( b in - A & b c= a )
let B be Element of SubstitutionSet (V,C); :: thesis: ( B = {a} & A ^ B = {} implies ex b being finite set st
( b in - A & b c= a ) )
assume A1: B = {a} ; :: thesis: ( not A ^ B = {} or ex b being finite set st
( b in - A & b c= a ) )
assume A2: A ^ B = {} ; :: thesis: ex b being finite set st
( b in - A & b c= a )

per cases ( not A is empty or A is empty ) ;

suppose A3: not A is empty ; :: thesis: ex b being finite set st
( b in - A & b c= a )

then reconsider AA = A as non empty finite set ;
defpred S₁[ Element of PFuncs (V,C), set ] means ( $2 in (dom $1) /\ (dom a) & $1 . $2 <> a . $2 );
defpred S₂[ set ] means verum;
A4: ex kk being Function st
( kk = a & dom kk c= V & rng kk c= C ) by PARTFUN1:def 3;

A5: now :: thesis: for s being Element of PFuncs (V,C) st s in A holds
ex x being Element of [V] st S₁[s,x]

let s be Element of PFuncs (V,C); :: thesis: ( s in A implies ex x being Element of [V] st S₁[s,x] )
assume A6: s in A ; :: thesis: ex x being Element of [V] st S₁[s,x]
not s tolerates a

proof

assume A7: s tolerates a ; :: thesis: contradiction
a in B by A1, TARSKI:def 1;
then s \/ a in { (s1 \/ t1) where s1, t1 is Element of PFuncs (V,C) : ( s1 in A & t1 in B & s1 tolerates t1 ) } by A6, A7;
hence contradiction by A2, SUBSTLAT:def 3; :: thesis: verum

end;

then consider x being object such that
A8: x in (dom s) /\ (dom a) and
A9: s . x <> a . x by PARTFUN1:def 4;
consider a9 being Function such that
A10: a9 = a and
A11: dom a9 c= V and
rng a9 c= C by PARTFUN1:def 3;
(dom s) /\ (dom a) c= dom a9 by A10, XBOOLE_1:17;
then (dom s) /\ (dom a) c= V by A11;
then reconsider x = x as Element of [V] by A8, HEYTING1:def 2;
take x = x; :: thesis: S₁[s,x]
thus S₁[s,x] by A8, A9; :: thesis: verum

end;

consider g being Element of Funcs ((PFuncs (V,C)),[V]) such that
A12: for s being Element of PFuncs (V,C) st s in A holds
S₁[s,g . s] from FRAENKEL:sch 27(A5);
deffunc H₁( set ) -> set = g . $1;
A13: A = [A] by A3, HEYTING1:def 2;
{ H₁(b) where b is Element of AA : S₂[b] } is finite from PRE_CIRC:sch 1();
then reconsider UKA = { (g . b) where b is Element of [A] : verum } as finite set by A13;
set f = a | UKA;
A14: dom (a | UKA) c= Involved A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (a | UKA) or x in Involved A )
assume x in dom (a | UKA) ; :: thesis: x in Involved A
then x in UKA by RELAT_1:57;
then consider b being Element of [A] such that
A15: x = g . b ;
reconsider b = b as finite Function by A13, Th1;
reconsider b9 = b as Element of PFuncs (V,C) by A13, SETWISEO:9;
g . b9 in (dom b9) /\ (dom a) by A13, A12;
then x in dom b by A15, XBOOLE_0:def 4;
hence x in Involved A by A13, Def1; :: thesis: verum

end;

rng (a | UKA) c= rng a by RELAT_1:70;
then rng (a | UKA) c= C by A4;
then reconsider f9 = a | UKA as Element of PFuncs ((Involved A),C) by A14, PARTFUN1:def 3;
for g being Element of PFuncs (V,C) st g in A holds
not a | UKA tolerates g

proof

let g1 be Element of PFuncs (V,C); :: thesis: ( g1 in A implies not a | UKA tolerates g1 )
reconsider g9 = g1 as Function ;
assume A16: g1 in A ; :: thesis: not a | UKA tolerates g1
ex z being set st
( z in (dom g1) /\ (dom (a | UKA)) & g9 . z <> (a | UKA) . z )

proof

set z = g . g1;
take g . g1 ; :: thesis: ( g . g1 in (dom g1) /\ (dom (a | UKA)) & g9 . (g . g1) <> (a | UKA) . (g . g1) )
A17: g . g1 in (dom g1) /\ (dom a) by A12, A16;
then A18: g . g1 in dom a by XBOOLE_0:def 4;
g . g1 in { (g . b1) where b1 is Element of [A] : verum } by A13, A16;
then g . g1 in (dom a) /\ UKA by A18, XBOOLE_0:def 4;
then A19: g . g1 in dom (a | UKA) by RELAT_1:61;
g . g1 in dom g1 by A17, XBOOLE_0:def 4;
hence g . g1 in (dom g1) /\ (dom (a | UKA)) by A19, XBOOLE_0:def 4; :: thesis: g9 . (g . g1) <> (a | UKA) . (g . g1)
g1 . (g . g1) <> a . (g . g1) by A12, A16;
hence g9 . (g . g1) <> (a | UKA) . (g . g1) by A19, FUNCT_1:47; :: thesis: verum

end;

hence not a | UKA tolerates g1 by PARTFUN1:def 4; :: thesis: verum

end;

then f9 in { f1 where f1 is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f1 tolerates g } ;
hence ex b being finite set st
( b in - A & b c= a ) by RELAT_1:59; :: thesis: verum

end;

suppose A20: A is empty ; :: thesis: ex b being finite set st
( b in - A & b c= a )

reconsider K = {} as finite set ;
take K ; :: thesis: ( K in - A & K c= a )
- A = {{}} by A20, Th10;
hence ( K in - A & K c= a ) by TARSKI:def 1; :: thesis: verum

end;

end;