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