let a, V be set ; :: thesis: for C being finite set
for A being Element of Fin (PFuncs V,C)
for K being Element of SubstitutionSet V,C st a in A ^ (A =>> K) holds
ex b being set st
( b in K & b c= a )
let C be finite set ; :: thesis: for A being Element of Fin (PFuncs V,C)
for K being Element of SubstitutionSet V,C st a in A ^ (A =>> K) holds
ex b being set st
( b in K & b c= a )
let A be Element of Fin (PFuncs V,C); :: thesis: for K being Element of SubstitutionSet V,C st a in A ^ (A =>> K) holds
ex b being set st
( b in K & b c= a )
let K be Element of SubstitutionSet V,C; :: thesis: ( a in A ^ (A =>> K) implies ex b being set st
( b in K & b c= a ) )
assume a in A ^ (A =>> K) ; :: thesis: ex b being set st
( b in K & b c= a )
then consider b, c being set such that
A1: b in A and
A2: c in A =>> K and
A3: a = b \/ c by SUBSTLAT:15;
consider f being PartFunc of A,K such that
A4: ( c = union { ((f . i) \ i) where i is Element of PFuncs V,C : i in A } & dom f = A ) by A2, Th20;
A5: f . b in K by A1, A4, PARTFUN1:27;
K c= PFuncs V,C by FINSUB_1:def 5;
then reconsider d = f . b as Element of PFuncs V,C by A5;
take d ; :: thesis: ( d in K & d c= a )
thus d in K by A1, A4, PARTFUN1:27; :: thesis: d c= a
A c= PFuncs V,C by FINSUB_1:def 5;
then reconsider b' = b as Element of PFuncs V,C by A1;
d \ b' in { ((f . i) \ i) where i is Element of PFuncs V,C : i in A } by A1;
hence d c= a by A3, A4, XBOOLE_1:44, ZFMISC_1:92; :: thesis: verum