let V be set ; :: thesis: for C being finite set
for u being Element of (SubstLatt V,C)
for a being Element of PFuncs V,C
for K being Element of Fin (PFuncs V,C) st a is finite & K = {a} holds
ex v being Element of SubstitutionSet V,C st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a ) )
let C be finite set ; :: thesis: for u being Element of (SubstLatt V,C)
for a being Element of PFuncs V,C
for K being Element of Fin (PFuncs V,C) st a is finite & K = {a} holds
ex v being Element of SubstitutionSet V,C st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a ) )
let u be Element of (SubstLatt V,C); :: thesis: for a being Element of PFuncs V,C
for K being Element of Fin (PFuncs V,C) st a is finite & K = {a} holds
ex v being Element of SubstitutionSet V,C st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a ) )
let a be Element of PFuncs V,C; :: thesis: for K being Element of Fin (PFuncs V,C) st a is finite & K = {a} holds
ex v being Element of SubstitutionSet V,C st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a ) )
let K be Element of Fin (PFuncs V,C); :: thesis: ( a is finite & K = {a} implies ex v being Element of SubstitutionSet V,C st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a ) ) )
assume A1: ( a is finite & K = {a} ) ; :: thesis: ex v being Element of SubstitutionSet V,C st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a ) )
defpred S₁[ Element of PFuncs V,C] means ( $1 is finite & not $1 tolerates a );
deffunc H₁( set ) -> set = $1;
set M = { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } ;
A2: { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } c= u from FRAENKEL:sch 17();
then reconsider v = { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } as Element of (SubstLatt V,C) by Th22;
reconsider v = v as Element of SubstitutionSet V,C by SUBSTLAT:def 4;
take v ; :: thesis: ( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a ) )
thus v in SUB u by A2; :: thesis: ( v ^ K = {} & ( for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a ) )
deffunc H₂( Element of PFuncs V,C, Element of PFuncs V,C) -> set = $1 \/ $2;
defpred S₂[ Element of PFuncs V,C, Element of PFuncs V,C] means ( $1 in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } & $2 in {a} & $1 tolerates $2 );
defpred S₃[ Element of PFuncs V,C, Element of PFuncs V,C] means ( $2 = a & $1 in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } & $1 tolerates $2 );
A3: for s, t being Element of PFuncs V,C holds
( S₂[s,t] iff S₃[s,t] ) by TARSKI:def 1;
A4: { H₂(s,t) where s, t is Element of PFuncs V,C : S₂[s,t] } = { H₂(s',t') where s', t' is Element of PFuncs V,C : S₃[s',t'] } from FRAENKEL:sch 4(A3);
defpred S₄[ Element of PFuncs V,C] means ( $1 in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } & $1 tolerates a );
defpred S₅[ Element of PFuncs V,C] means ( not $1 tolerates a & $1 in u & $1 tolerates a );
for s being Element of PFuncs V,C holds
( s in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } iff ( s is finite & not s tolerates a & s in u ) )

proof

let s be Element of PFuncs V,C; :: thesis: ( s in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } iff ( s is finite & not s tolerates a & s in u ) )
thus ( s in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } implies ( s is finite & not s tolerates a & s in u ) ) :: thesis: ( s is finite & not s tolerates a & s in u implies s in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } )

proof

assume s in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } ; :: thesis: ( s is finite & not s tolerates a & s in u )
then consider s2 being Element of PFuncs V,C such that
A5: ( s2 = s & s2 in u & s2 is finite & not s2 tolerates a ) ;
thus ( s is finite & not s tolerates a & s in u ) by A5; :: thesis: verum

end;

thus ( s is finite & not s tolerates a & s in u implies s in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } ) ; :: thesis: verum

end;

then A6: for s being Element of PFuncs V,C holds
( S₄[s] iff S₅[s] ) ;
deffunc H₃( Element of PFuncs V,C, Element of PFuncs V,C) -> set = $1 \/ $2;
defpred S₆[ Element of PFuncs V,C, Element of PFuncs V,C] means ( $1 in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } & $1 tolerates $2 );
A7: { H₃(s,t) where s, t is Element of PFuncs V,C : ( t = a & S₆[s,t] ) } = { H₃(s',a) where s' is Element of PFuncs V,C : S₆[s',a] } from FRAENKEL:sch 20();
deffunc H₄( Element of PFuncs V,C) -> set = $1 \/ a;
{ H₄(s') where s' is Element of PFuncs V,C : S₄[s'] } = { H₄(s) where s is Element of PFuncs V,C : S₅[s] } from FRAENKEL:sch 3(A6);
then A8: v ^ K = { (s \/ a) where s is Element of PFuncs V,C : ( not s tolerates a & s in u & s tolerates a ) } by A1, A4, A7, SUBSTLAT:def 3;
thus v ^ K = {} :: thesis: for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a

proof

assume v ^ K <> {} ; :: thesis: contradiction
then consider x being set such that
A9: x in v ^ K by XBOOLE_0:def 1;
consider s1 being Element of PFuncs V,C such that
A10: ( x = s1 \/ a & not s1 tolerates a & s1 in u & s1 tolerates a ) by A8, A9;
thus contradiction by A10; :: thesis: verum

end;

let b be Element of PFuncs V,C; :: thesis: ( b in (diff u) . v implies b tolerates a )
assume b in (diff u) . v ; :: thesis: b tolerates a
then A11: b in u \ v by Def7;
then A12: ( b in u & not b in { H₁(s) where s is Element of PFuncs V,C : ( H₁(s) in u & S₁[s] ) } ) by XBOOLE_0:def 5;
u in the carrier of (SubstLatt V,C) ;
then u in SubstitutionSet V,C by SUBSTLAT:def 4;
then b is finite by A11, Th2;
hence b tolerates a by A12; :: thesis: verum