let V be set ; :: thesis: for C being finite set
for a being Element of PFuncs V,C
for u, v being Element of SubstitutionSet V,C st ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) holds
ex b being set st
( b in u =>> v & b c= a )
let C be finite set ; :: thesis: for a being Element of PFuncs V,C
for u, v being Element of SubstitutionSet V,C st ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) holds
ex b being set st
( b in u =>> v & b c= a )
let a be Element of PFuncs V,C; :: thesis: for u, v being Element of SubstitutionSet V,C st ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) holds
ex b being set st
( b in u =>> v & b c= a )
let u, v be Element of SubstitutionSet V,C; :: thesis: ( ( for c being set st c in u holds
ex b being set st
( b in v & b c= c \/ a ) ) implies ex b being set st
( b in u =>> v & b c= a ) )
reconsider u9 = u as Element of (SubstLatt V,C) by SUBSTLAT:def 4;
defpred S₁[ set , set ] means ( $2 in v & $2 c= $1 \/ a );
assume A1: for b being set st b in u holds
ex c being set st
( c in v & c c= b \/ a ) ; :: thesis: ex b being set st
( b in u =>> v & b c= a )

A2: now

let b be Element of PFuncs V,C; :: thesis: ( b in u implies ex x being Element of PFuncs V,C st S₁[b,x] )
assume b in u ; :: thesis: ex x being Element of PFuncs V,C st S₁[b,x]
then consider c being set such that
A3: c in v and
A4: c c= b \/ a by A1;
v c= PFuncs V,C by FINSUB_1:def 5;
then reconsider c = c as Element of PFuncs V,C by A3;
take x = c; :: thesis: S₁[b,x]
thus S₁[b,x] by A3, A4; :: thesis: verum

end;

consider f9 being Element of Funcs (PFuncs V,C),(PFuncs V,C) such that
A5: for b being Element of PFuncs V,C st b in u holds
S₁[b,f9 . b] from FRAENKEL:sch 27(A2);
set g = f9 | u;
consider f2 being Function such that
A6: f9 = f2 and
dom f2 = PFuncs V,C and
rng f2 c= PFuncs V,C by FUNCT_2:def 2;
u c= PFuncs V,C by FINSUB_1:def 5;
then f9 | u is Function of u,(PFuncs V,C) by FUNCT_2:38;
then A7: dom (f9 | u) = u by FUNCT_2:def 1;
for b being set st b in u holds
(f9 | u) . b in v

proof

let b be set ; :: thesis: ( b in u implies (f9 | u) . b in v )
assume A8: b in u ; :: thesis: (f9 | u) . b in v
u c= PFuncs V,C by FINSUB_1:def 5;
then reconsider b9 = b as Element of PFuncs V,C by A8;
(f9 | u) . b9 = f2 . b9 by A6, A8, FUNCT_1:72;
hence (f9 | u) . b in v by A5, A6, A8; :: thesis: verum

end;

then f9 | u is Function of u,v by A7, FUNCT_2:5;
then A9: rng (f9 | u) c= v by RELAT_1:def 19;
A10: for b being set st b in u9 holds
(f9 | u) . b c= b \/ a

proof

let b be set ; :: thesis: ( b in u9 implies (f9 | u) . b c= b \/ a )
assume A11: b in u9 ; :: thesis: (f9 | u) . b c= b \/ a
u c= PFuncs V,C by FINSUB_1:def 5;
then reconsider b9 = b as Element of PFuncs V,C by A11;
(f9 | u) . b9 = f2 . b9 by A6, A11, FUNCT_1:72;
hence (f9 | u) . b c= b \/ a by A5, A6, A11; :: thesis: verum

end;

reconsider g = f9 | u as Element of PFuncs u,v by A7, A9, PARTFUN1:def 5;
set d = union { ((g . i) \ i) where i is Element of PFuncs V,C : i in u9 } ;
A12: union { ((g . i) \ i) where i is Element of PFuncs V,C : i in u9 } c= a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { ((g . i) \ i) where i is Element of PFuncs V,C : i in u9 } or x in a )
assume x in union { ((g . i) \ i) where i is Element of PFuncs V,C : i in u9 } ; :: thesis: x in a
then consider Y being set such that
A13: x in Y and
A14: Y in { ((g . i) \ i) where i is Element of PFuncs V,C : i in u9 } by TARSKI:def 4;
consider j being Element of PFuncs V,C such that
A15: Y = (g . j) \ j and
A16: j in u9 by A14;
g . j c= j \/ a by A10, A16;
then (g . j) \ j c= a by XBOOLE_1:43;
hence x in a by A13, A15; :: thesis: verum

end;

then reconsider d = union { ((g . i) \ i) where i is Element of PFuncs V,C : i in u9 } as Element of PFuncs V,C by PRE_POLY:15;
take d ; :: thesis: ( d in u =>> v & d c= a )
d in { (union { ((f . i) \ i) where i is Element of PFuncs V,C : i in u } ) where f is Element of PFuncs u,v : dom f = u } by A7;
hence d in u =>> v by XBOOLE_0:def 4; :: thesis: d c= a
thus d c= a by A12; :: thesis: verum