defpred S1[ Function, Function] means for f being SCBinominativeFunction of V,A st f = $1 holds
( dom $2 = dom f & ( for d being TypeSCNominativeData of V,A st d in dom $2 holds
$2 . d = local_overlapping (V,A,d,($1 . d),v) ) );
A1:
for x being Element of FPrg (ND (V,A)) ex y being Element of FPrg (ND (V,A)) st S1[x,y]
proof
let x be
Element of
FPrg (ND (V,A));
ex y being Element of FPrg (ND (V,A)) st S1[x,y]
defpred S2[
object ,
object ]
means $2
= local_overlapping (
V,
A,$1,
(x . $1),
v);
A2:
for
a being
object st
a in dom x holds
ex
y being
object st
(
y in ND (
V,
A) &
S2[
a,
y] )
consider F being
Function such that A3:
dom F = dom x
and A4:
rng F c= ND (
V,
A)
and A5:
for
a being
object st
a in dom x holds
S2[
a,
F . a]
from FUNCT_1:sch 6(A2);
F is
PartFunc of
(ND (V,A)),
(ND (V,A))
by A3, A4, RELSET_1:4, RELAT_1:def 18;
then reconsider F =
F as
Element of
FPrg (ND (V,A)) by PARTFUN1:45;
take
F
;
S1[x,F]
thus
S1[
x,
F]
by A3, A5;
verum
end;
consider F being Function of (FPrg (ND (V,A))),(FPrg (ND (V,A))) such that
A6:
for x being Element of FPrg (ND (V,A)) holds S1[x,F . x]
from FUNCT_2:sch 3(A1);
take
F
; for f being SCBinominativeFunction of V,A holds
( dom (F . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (F . f) holds
(F . f) . d = local_overlapping (V,A,d,(f . d),v) ) )
let f be SCBinominativeFunction of V,A; ( dom (F . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (F . f) holds
(F . f) . d = local_overlapping (V,A,d,(f . d),v) ) )
f in FPrg (ND (V,A))
by PARTFUN1:45;
hence
( dom (F . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (F . f) holds
(F . f) . d = local_overlapping (V,A,d,(f . d),v) ) )
by A6; verum