defpred S₁[ object , object , object ] means for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A st $1 = p & $2 = f holds
for F being Function st F = $3 holds
( dom F = H₁(p,f) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = p . (local_overlapping (V,A,d,(f . d),v)) ) );
A1: for x1, x2 being object st x1 in Pr (ND (V,A)) & x2 in FPrg (ND (V,A)) holds
ex y being object st
( y in Pr (ND (V,A)) & S₁[x1,x2,y] )

proof

let x1, x2 be object ; :: thesis: ( x1 in Pr (ND (V,A)) & x2 in FPrg (ND (V,A)) implies ex y being object st
( y in Pr (ND (V,A)) & S₁[x1,x2,y] ) )
assume x1 in Pr (ND (V,A)) ; :: thesis: ( not x2 in FPrg (ND (V,A)) or ex y being object st
( y in Pr (ND (V,A)) & S₁[x1,x2,y] ) )
then reconsider X1 = x1 as PartFunc of (ND (V,A)),BOOLEAN by PARTFUN1:46;
assume x2 in FPrg (ND (V,A)) ; :: thesis: ex y being object st
( y in Pr (ND (V,A)) & S₁[x1,x2,y] )
then reconsider X2 = x2 as PartFunc of (ND (V,A)),(ND (V,A)) by PARTFUN1:46;
defpred S₂[ object , object ] means for d being TypeSCNominativeData of V,A st d = $1 & local_overlapping (V,A,d,(X2 . d),v) in dom X1 holds
$2 = X1 . (local_overlapping (V,A,d,(X2 . d),v));
A2: for a being object st a in H₁(X1,X2) holds
ex b being object st
( b in BOOLEAN & S₂[a,b] )

proof

let a be object ; :: thesis: ( a in H₁(X1,X2) implies ex b being object st
( b in BOOLEAN & S₂[a,b] ) )
assume a in H₁(X1,X2) ; :: thesis: ex b being object st
( b in BOOLEAN & S₂[a,b] )
then consider d being TypeSCNominativeData of V,A such that
A3: ( d = a & local_overlapping (V,A,d,(X2 . d),v) in dom X1 & d in dom X2 ) ;
take X1 . (local_overlapping (V,A,d,(X2 . d),v)) ; :: thesis: ( X1 . (local_overlapping (V,A,d,(X2 . d),v)) in BOOLEAN & S₂[a,X1 . (local_overlapping (V,A,d,(X2 . d),v))] )
thus ( X1 . (local_overlapping (V,A,d,(X2 . d),v)) in BOOLEAN & S₂[a,X1 . (local_overlapping (V,A,d,(X2 . d),v))] ) by A3, PARTFUN1:4; :: thesis: verum

end;

consider K being Function such that
A4: dom K = H₁(X1,X2) and
A5: rng K c= BOOLEAN and
A6: for x being object st x in H₁(X1,X2) holds
S₂[x,K . x] from FUNCT_1:sch 6(A2);
take K ; :: thesis: ( K in Pr (ND (V,A)) & S₁[x1,x2,K] )
H₁(X1,X2) c= ND (V,A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₁(X1,X2) or x in ND (V,A) )
assume x in H₁(X1,X2) ; :: thesis: x in ND (V,A)
then ex d being TypeSCNominativeData of V,A st
( d = x & local_overlapping (V,A,d,(X2 . d),v) in dom X1 & d in dom X2 ) ;
hence x in ND (V,A) ; :: thesis: verum

end;

then K is PartFunc of (ND (V,A)),BOOLEAN by A4, A5, RELSET_1:4;
hence K in Pr (ND (V,A)) by PARTFUN1:45; :: thesis: S₁[x1,x2,K]
let p be SCPartialNominativePredicate of V,A; :: thesis: for f being SCBinominativeFunction of V,A st x1 = p & x2 = f holds
for F being Function st F = K holds
( dom F = H₁(p,f) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = p . (local_overlapping (V,A,d,(f . d),v)) ) )
let f be SCBinominativeFunction of V,A; :: thesis: ( x1 = p & x2 = f implies for F being Function st F = K holds
( dom F = H₁(p,f) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = p . (local_overlapping (V,A,d,(f . d),v)) ) ) )
assume A7: ( x1 = p & x2 = f ) ; :: thesis: for F being Function st F = K holds
( dom F = H₁(p,f) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = p . (local_overlapping (V,A,d,(f . d),v)) ) )
let F be Function; :: thesis: ( F = K implies ( dom F = H₁(p,f) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = p . (local_overlapping (V,A,d,(f . d),v)) ) ) )
assume A8: F = K ; :: thesis: ( dom F = H₁(p,f) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = p . (local_overlapping (V,A,d,(f . d),v)) ) )
thus dom F = H₁(p,f) by A4, A7, A8; :: thesis: for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = p . (local_overlapping (V,A,d,(f . d),v))
let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom F implies F . d = p . (local_overlapping (V,A,d,(f . d),v)) )
assume A9: d in dom F ; :: thesis: F . d = p . (local_overlapping (V,A,d,(f . d),v))
then ex d1 being TypeSCNominativeData of V,A st
( d1 = d & local_overlapping (V,A,d1,(X2 . d1),v) in dom X1 & d1 in dom X2 ) by A4, A8;
hence F . d = p . (local_overlapping (V,A,d,(f . d),v)) by A4, A6, A7, A8, A9; :: thesis: verum

end;

consider F being Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))) such that
A10: for x, y being object st x in Pr (ND (V,A)) & y in FPrg (ND (V,A)) holds
S₁[x,y,F . (x,y)] from BINOP_1:sch 1(A1);
take F ; :: thesis: for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds
( dom (F . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds
F . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) )
let p be SCPartialNominativePredicate of V,A; :: thesis: for f being SCBinominativeFunction of V,A holds
( dom (F . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds
F . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) )
let f be SCBinominativeFunction of V,A; :: thesis: ( dom (F . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds
F . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) )
A11: ( p in Pr (ND (V,A)) & f in FPrg (ND (V,A)) ) by PARTFUN1:45;
hence A12: dom (F . (p,f)) = H₁(p,f) by A10; :: thesis: for d being TypeSCNominativeData of V,A st d in dom f holds
F . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v)
let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom f implies F . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) )
assume A13: d in dom f ; :: thesis: F . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v)
thus ( d in dom (F . (p,f)) iff local_overlapping (V,A,d,(f . d),v) in dom p ) :: according to NOMIN_1:def 1 :: thesis: ( not d in dom (F . (p,f)) or (F . (p,f)) . d = p . (local_overlapping (V,A,d,(f . d),v)) )

proof

hereby :: thesis: ( local_overlapping (V,A,d,(f . d),v) in dom p implies d in dom (F . (p,f)) )

assume d in dom (F . (p,f)) ; :: thesis: local_overlapping (V,A,d,(f . d),v) in dom p
then ex d1 being TypeSCNominativeData of V,A st
( d = d1 & local_overlapping (V,A,d1,(f . d1),v) in dom p & d1 in dom f ) by A12;
hence local_overlapping (V,A,d,(f . d),v) in dom p ; :: thesis: verum

end;

thus ( local_overlapping (V,A,d,(f . d),v) in dom p implies d in dom (F . (p,f)) ) by A12, A13; :: thesis: verum

end;

thus ( not d in dom (F . (p,f)) or (F . (p,f)) . d = p . (local_overlapping (V,A,d,(f . d),v)) ) by A10, A11; :: thesis: verum