defpred S2[ object , object , object ] means for f being SCBinominativeFunction of V,A
for x being Element of product g st $1 = f & $2 = x holds
for h being Function st h = $3 holds
( dom h = H1(f) & ( for d being TypeSCNominativeData of V,A st d in dom h holds
h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) );
A2: for x1, x2 being object st x1 in FPrg (ND (V,A)) & x2 in product g holds
ex y being object st
( y in FPrg (ND (V,A)) & S2[x1,x2,y] )
proof
let x1, x2 be object ; :: thesis: ( x1 in FPrg (ND (V,A)) & x2 in product g implies ex y being object st
( y in FPrg (ND (V,A)) & S2[x1,x2,y] ) )
assume x1 in FPrg (ND (V,A)) ; :: thesis: ( not x2 in product g or ex y being object st
( y in FPrg (ND (V,A)) & S2[x1,x2,y] ) )
then reconsider X1 = x1 as PartFunc of (ND (V,A)),(ND (V,A)) by PARTFUN1:46;
assume x2 in product g ; :: thesis: ex y being object st
( y in FPrg (ND (V,A)) & S2[x1,x2,y] )
defpred S3[ object , object ] means for d being TypeSCNominativeData of V,A st d = $1 & global_overlapping (V,A,d,(NDentry (g,X,d))) in dom X1 holds
$2 = X1 . (global_overlapping (V,A,d,(NDentry (g,X,d))));
A3: for a being object st a in H1(X1) holds
ex b being object st
( b in ND (V,A) & S3[a,b] )
proof
let a be object ; :: thesis: ( a in H1(X1) implies ex b being object st
( b in ND (V,A) & S3[a,b] ) )
assume a in H1(X1) ; :: thesis: ex b being object st
( b in ND (V,A) & S3[a,b] )
then consider d being TypeSCNominativeData of V,A such that
A4: ( d = a & global_overlapping (V,A,d,(NDentry (g,X,d))) in dom X1 & S1[d] ) ;
take X1 . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ; :: thesis: ( X1 . (global_overlapping (V,A,d,(NDentry (g,X,d)))) in ND (V,A) & S3[a,X1 . (global_overlapping (V,A,d,(NDentry (g,X,d))))] )
thus ( X1 . (global_overlapping (V,A,d,(NDentry (g,X,d)))) in ND (V,A) & S3[a,X1 . (global_overlapping (V,A,d,(NDentry (g,X,d))))] ) by A4, PARTFUN1:4; :: thesis: verum
end;
consider K being Function such that
A5: dom K = H1(X1) and
A6: rng K c= ND (V,A) and
A7: for x being object st x in H1(X1) holds
S3[x,K . x] from FUNCT_1:sch 6(A3);
 take K ; :: thesis: ( K in FPrg (ND (V,A)) & S2[x1,x2,K] )
H1(X1) c= ND (V,A)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(X1) or x in ND (V,A) )
assume x in H1(X1) ; :: thesis: x in ND (V,A)
then ex d being TypeSCNominativeData of V,A st
( d = x & global_overlapping (V,A,d,(NDentry (g,X,d))) in dom X1 & S1[d] ) ;
hence x in ND (V,A) ; :: thesis: verum
end;
then K is PartFunc of (ND (V,A)),(ND (V,A)) by A5, A6, RELSET_1:4;
hence K in FPrg (ND (V,A)) by PARTFUN1:45; :: thesis: S2[x1,x2,K]
let f be SCBinominativeFunction of V,A; :: thesis: for x being Element of product g st x1 = f & x2 = x holds
for h being Function st h = K holds
( dom h = H1(f) & ( for d being TypeSCNominativeData of V,A st d in dom h holds
h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) )
let q be Element of product g; :: thesis: ( x1 = f & x2 = q implies for h being Function st h = K holds
( dom h = H1(f) & ( for d being TypeSCNominativeData of V,A st d in dom h holds
h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) ) )
assume A8: ( x1 = f & x2 = q ) ; :: thesis: for h being Function st h = K holds
( dom h = H1(f) & ( for d being TypeSCNominativeData of V,A st d in dom h holds
h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) )
let h be Function; :: thesis: ( h = K implies ( dom h = H1(f) & ( for d being TypeSCNominativeData of V,A st d in dom h holds
h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) ) )
assume A9: h = K ; :: thesis: ( dom h = H1(f) & ( for d being TypeSCNominativeData of V,A st d in dom h holds
h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) )
thus dom h = H1(f) by A5, A8, A9; :: thesis: for d being TypeSCNominativeData of V,A st d in dom h holds
h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d))))
let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom h implies h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
assume A10: d in dom h ; :: thesis: h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d))))
then ex d1 being TypeSCNominativeData of V,A st
( d1 = d & global_overlapping (V,A,d1,(NDentry (g,X,d1))) in dom X1 & S1[d1] ) by A5, A9;
hence h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) by A5, A7, A8, A9, A10; :: thesis: verum
end;
consider F being Function of [:(FPrg (ND (V,A))),(product g):],(FPrg (ND (V,A))) such that
A11: for x, y being object st x in FPrg (ND (V,A)) & y in product g holds
S2[x,y,F . (x,y)] from BINOP_1:sch 1(A2);
 take F ; :: thesis: for f being SCBinominativeFunction of V,A
for x being Element of product g holds
( dom (F . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
F . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) )
let f be SCBinominativeFunction of V,A; :: thesis: for x being Element of product g holds
( dom (F . (f,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
F . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) )
let q be Element of product g; :: thesis: ( dom (F . (f,q)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
F . (f,q),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) ) )
A12: ( f in FPrg (ND (V,A)) & q in product g ) by A1, PARTFUN1:45;
hence A13: dom (F . (f,q)) = H1(f) by A11; :: thesis: for d being TypeSCNominativeData of V,A st d in_doms g holds
F . (f,q),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d)))
let d be TypeSCNominativeData of V,A; :: thesis: ( d in_doms g implies F . (f,q),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) )
assume A14: S1[d] ; :: thesis: F . (f,q),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d)))
thus ( d in dom (F . (f,q)) iff global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f ) :: according to NOMIN_1:def 1 :: thesis: ( not d in dom (F . (f,q)) or (F . (f,q)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
proof
hereby :: thesis: ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f implies d in dom (F . (f,q)) )
assume d in dom (F . (f,q)) ; :: thesis: global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f
then ex d1 being TypeSCNominativeData of V,A st
( d = d1 & global_overlapping (V,A,d1,(NDentry (g,X,d1))) in dom f & S1[d1] ) by A13;
hence global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f ; :: thesis: verum
end;
thus ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f implies d in dom (F . (f,q)) ) by A13, A14; :: thesis: verum
end;
thus ( not d in dom (F . (f,q)) or (F . (f,q)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) by A11, A12; :: thesis: verum