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 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 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 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 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 ) )
deffunc H1( set ) -> set = $1;
let K be Element of Fin (PFuncs V,C); :: thesis: ( 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: 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 ) )
deffunc H2( Element of PFuncs V,C, Element of PFuncs V,C) -> set = $1 \/ $2;
defpred S1[ Element of PFuncs V,C] means ( not $1 tolerates a & $1 in u & $1 tolerates a );
deffunc H3( Element of PFuncs V,C, Element of PFuncs V,C) -> set = $1 \/ $2;
defpred S2[ Element of PFuncs V,C] means ( $1 is finite & not $1 tolerates a );
set M = { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } ;
defpred S3[ Element of PFuncs V,C, Element of PFuncs V,C] means ( $1 in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } & $2 in {a} & $1 tolerates $2 );
defpred S4[ Element of PFuncs V,C, Element of PFuncs V,C] means ( $2 = a & $1 in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } & $1 tolerates $2 );
defpred S5[ Element of PFuncs V,C] means ( $1 in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } & $1 tolerates a );
defpred S6[ Element of PFuncs V,C, Element of PFuncs V,C] means ( $1 in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } & $1 tolerates $2 );
deffunc H4( Element of PFuncs V,C) -> set = $1 \/ a;
A2: { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } c= u from FRAENKEL:sch 17();
 then reconsider v = { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[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 ) )
A3: for s, t being Element of PFuncs V,C holds
( S3[s,t] iff S4[s,t] ) by TARSKI:def 1;
A4: { H3(s,t) where s, t is Element of PFuncs V,C : S3[s,t] } = { H3(s',t') where s', t' is Element of PFuncs V,C : S4[s',t'] } from FRAENKEL:sch 4(A3);
 for s being Element of PFuncs V,C holds
( s in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } iff ( s is finite & not s tolerates a & s in u ) )
proof
let s be Element of PFuncs V,C; :: thesis: ( s in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } iff ( s is finite & not s tolerates a & s in u ) )
thus ( s in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[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 { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } )
proof
assume s in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } ; :: thesis: ( s is finite & not s tolerates a & s in u )
then ex s2 being Element of PFuncs V,C st
( s2 = s & s2 in u & s2 is finite & not s2 tolerates a ) ;
hence ( s is finite & not s tolerates a & s in u ) ; :: thesis: verum
end;
thus ( s is finite & not s tolerates a & s in u implies s in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[s] ) } ) ; :: thesis: verum
end;
then A5: for s being Element of PFuncs V,C holds
( S5[s] iff S1[s] ) ;
A6: { H4(s') where s' is Element of PFuncs V,C : S5[s'] } = { H4(s) where s is Element of PFuncs V,C : S1[s] } from FRAENKEL:sch 3(A5);
 { H2(s,t) where s, t is Element of PFuncs V,C : ( t = a & S6[s,t] ) } = { H2(s',a) where s' is Element of PFuncs V,C : S6[s',a] } from FRAENKEL:sch 20();
 then A7: 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, A6, 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
A8: x in v ^ K by XBOOLE_0:def 1;
ex s1 being Element of PFuncs V,C st
( x = s1 \/ a & not s1 tolerates a & s1 in u & s1 tolerates a ) by A7, A8;
hence contradiction ; :: 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 A9: b in u \ v by Def7;
then A10: not b in { H1(s) where s is Element of PFuncs V,C : ( H1(s) in u & S2[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 A9, Th2;
hence b tolerates a by A9, A10; :: thesis: verum