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 ;
( 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))
;
( 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
;
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 ;
( a in H1(X1) implies ex b being object st
( b in ND (V,A) & S3[a,b] ) )
assume
a in H1(
X1)
;
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))))
;
( 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;
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
;
( K in FPrg (ND (V,A)) & S2[x1,x2,K] )
H1(
X1)
c= ND (
V,
A)
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;
S2[x1,x2,K]
let f be
SCBinominativeFunction of
V,
A;
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;
( 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 )
;
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;
( 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
;
( 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;
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;
( d in dom h implies h . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
assume A10:
d in dom h
;
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;
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
; 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; 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; ( 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; 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; ( d in_doms g implies F . (f,q),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) )
assume A14:
S1[d]
; 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 )
NOMIN_1:def 1 ( not d in dom (F . (f,q)) or (F . (f,q)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )proof
hereby ( 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))
;
global_overlapping (V,A,d,(NDentry (g,X,d))) in dom fthen
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
;
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;
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; verum