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

proof

let x1, x2 be object ; :: thesis: ( x1 in FPrg (ND (V,A)) & x2 in FPrg (ND (V,A)) implies ex y being object st
( y in FPrg (ND (V,A)) & S₁[x1,x2,y] ) )
assume x1 in FPrg (ND (V,A)) ; :: thesis: ( not x2 in FPrg (ND (V,A)) or ex y being object st
( y in FPrg (ND (V,A)) & S₁[x1,x2,y] ) )
then reconsider X1 = x1 as PartFunc of (ND (V,A)),(ND (V,A)) by PARTFUN1:46;
assume x2 in FPrg (ND (V,A)) ; :: thesis: ex y being object st
( y in FPrg (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 ND (V,A) & S₂[a,b] )

proof

let a be object ; :: thesis: ( a in H₁(X1,X2) implies ex b being object st
( b in ND (V,A) & S₂[a,b] ) )
assume a in H₁(X1,X2) ; :: thesis: ex b being object st
( b in ND (V,A) & 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 ND (V,A) & S₂[a,X1 . (local_overlapping (V,A,d,(X2 . d),v))] )
thus ( X1 . (local_overlapping (V,A,d,(X2 . d),v)) in ND (V,A) & 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= ND (V,A) 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 FPrg (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)),(ND (V,A)) by A4, A5, RELSET_1:4;
hence K in FPrg (ND (V,A)) by PARTFUN1:45; :: thesis: S₁[x1,x2,K]
let f, g be SCBinominativeFunction of V,A; :: thesis: ( x1 = f & x2 = g implies for F being Function st F = K holds
( dom F = H₁(f,g) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = f . (local_overlapping (V,A,d,(g . d),v)) ) ) )
assume A7: ( x1 = f & x2 = g ) ; :: thesis: for F being Function st F = K holds
( dom F = H₁(f,g) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = f . (local_overlapping (V,A,d,(g . d),v)) ) )
let F be Function; :: thesis: ( F = K implies ( dom F = H₁(f,g) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = f . (local_overlapping (V,A,d,(g . d),v)) ) ) )
assume A8: F = K ; :: thesis: ( dom F = H₁(f,g) & ( for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = f . (local_overlapping (V,A,d,(g . d),v)) ) )
thus dom F = H₁(f,g) by A4, A7, A8; :: thesis: for d being TypeSCNominativeData of V,A st d in dom F holds
F . d = f . (local_overlapping (V,A,d,(g . d),v))
let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom F implies F . d = f . (local_overlapping (V,A,d,(g . d),v)) )
assume A9: d in dom F ; :: thesis: F . d = f . (local_overlapping (V,A,d,(g . 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 = f . (local_overlapping (V,A,d,(g . d),v)) by A4, A6, A7, A8, A9; :: thesis: verum

end;

consider F being Function of [:(FPrg (ND (V,A))),(FPrg (ND (V,A))):],(FPrg (ND (V,A))) such that
A10: for x, y being object st x in FPrg (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 f, g being SCBinominativeFunction of V,A holds
( dom (F . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds
F . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) )
let f, g be SCBinominativeFunction of V,A; :: thesis: ( dom (F . (f,g)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } & ( for d being TypeSCNominativeData of V,A st d in dom g holds
F . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) ) )
A11: ( f in FPrg (ND (V,A)) & g in FPrg (ND (V,A)) ) by PARTFUN1:45;
hence A12: dom (F . (f,g)) = H₁(f,g) by A10; :: thesis: for d being TypeSCNominativeData of V,A st d in dom g holds
F . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v)
let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom g implies F . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v) )
assume A13: d in dom g ; :: thesis: F . (f,g),d =~ f, local_overlapping (V,A,d,(g . d),v)
thus ( d in dom (F . (f,g)) iff local_overlapping (V,A,d,(g . d),v) in dom f ) :: according to NOMIN_1:def 1 :: thesis: ( not d in dom (F . (f,g)) or (F . (f,g)) . d = f . (local_overlapping (V,A,d,(g . d),v)) )

proof

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

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

end;

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

end;

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