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 ) )
A1: K c= PFuncs (V,C) by FINSUB_1:def 5;
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
A2: b in A and
A3: c in A =>> K and
A4: a = b \/ c by SUBSTLAT:15;
A c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider b9 = b as Element of PFuncs (V,C) by A2;
consider f being PartFunc of A,K such that
A5: c = union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } and
A6: dom f = A by A3, Th15;
f . b in K by A2, A6, PARTFUN1:4;
then reconsider d = f . b as Element of PFuncs (V,C) by A1;
take d ; :: thesis: ( d in K & d c= a )
thus d in K by A2, A6, PARTFUN1:4; :: thesis: d c= a
d \ b9 in { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } by A2;
hence d c= a by A4, A5, XBOOLE_1:44, ZFMISC_1:74; :: thesis: verum