defpred S₁[ 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 S₁[x,y]

proof

let x be Element of FPrg (ND (V,A)); :: thesis: ex y being Element of FPrg (ND (V,A)) st S₁[x,y]
defpred S₂[ 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) & S₂[a,y] )

proof

let a be object ; :: thesis: ( a in dom x implies ex y being object st
( y in ND (V,A) & S₂[a,y] ) )
local_overlapping (V,A,a,(x . a),v) in ND (V,A) ;
hence ( a in dom x implies ex y being object st
( y in ND (V,A) & S₂[a,y] ) ) ; :: thesis: verum

end;

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
S₂[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 ; :: thesis: S₁[x,F]
thus S₁[x,F] by A3, A5; :: thesis: 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 S₁[x,F . x] from FUNCT_2:sch 3(A1);
take F ; :: thesis: 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; :: thesis: ( 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; :: thesis: verum