let v be object ; for V, A being set
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A
for x being Element of product <*f*> st v in V & product <*f*> <> {} holds
SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>)
let V, A be set ; for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A
for x being Element of product <*f*> st v in V & product <*f*> <> {} holds
SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>)
let p be SCPartialNominativePredicate of V,A; for f being SCBinominativeFunction of V,A
for x being Element of product <*f*> st v in V & product <*f*> <> {} holds
SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>)
let f be SCBinominativeFunction of V,A; for x being Element of product <*f*> st v in V & product <*f*> <> {} holds
SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>)
set g = <*f*>;
let x be Element of product <*f*>; ( v in V & product <*f*> <> {} implies SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>) )
assume that
A1:
v in V
and
A2:
product <*f*> <> {}
; SC_Psuperpos (p,f,v) = SC_Psuperpos (p,x,<*v*>)
set X = <*v*>;
set S1 = SC_Psuperpos (p,f,v);
set S2 = SC_Psuperpos (p,x,<*v*>);
defpred S1[ object ] means $1 in_doms <*f*>;
A3:
<*f*> . 1 = f
by FINSEQ_1:40;
A4:
dom <*f*> = {1}
by FINSEQ_1:2, FINSEQ_1:38;
A5:
dom (SC_Psuperpos (p,f,v)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) }
by Def11;
SC_Psuperpos (p,x,<*v*>) = (SCPsuperpos (<*f*>,<*v*>)) . (p,x)
by A2, Def10;
then A6:
dom (SC_Psuperpos (p,x,<*v*>)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (<*f*>,<*v*>,d))) in dom p & S1[d] ) }
by A2, Def9;
thus A7:
dom (SC_Psuperpos (p,f,v)) = dom (SC_Psuperpos (p,x,<*v*>))
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (SC_Psuperpos (p,f,v)) or (SC_Psuperpos (p,f,v)) . b1 = (SC_Psuperpos (p,x,<*v*>)) . b1 )proof
thus
dom (SC_Psuperpos (p,f,v)) c= dom (SC_Psuperpos (p,x,<*v*>))
XBOOLE_0:def 10 dom (SC_Psuperpos (p,x,<*v*>)) c= dom (SC_Psuperpos (p,f,v))proof
let a be
object ;
TARSKI:def 3 ( not a in dom (SC_Psuperpos (p,f,v)) or a in dom (SC_Psuperpos (p,x,<*v*>)) )
assume
a in dom (SC_Psuperpos (p,f,v))
;
a in dom (SC_Psuperpos (p,x,<*v*>))
then consider d being
TypeSCNominativeData of
V,
A such that A8:
d = a
and A9:
local_overlapping (
V,
A,
d,
(f . d),
v)
in dom p
and A10:
d in dom f
by A5;
A11:
S1[
d]
NDentry (
<*f*>,
<*v*>,
d)
= naming (
V,
A,
v,
(f . d))
by A1, A10, Th26;
hence
a in dom (SC_Psuperpos (p,x,<*v*>))
by A8, A9, A11, A6;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in dom (SC_Psuperpos (p,x,<*v*>)) or a in dom (SC_Psuperpos (p,f,v)) )
assume
a in dom (SC_Psuperpos (p,x,<*v*>))
;
a in dom (SC_Psuperpos (p,f,v))
then consider d being
TypeSCNominativeData of
V,
A such that A12:
a = d
and A13:
global_overlapping (
V,
A,
d,
(NDentry (<*f*>,<*v*>,d)))
in dom p
and A14:
S1[
d]
by A6;
1
in dom <*f*>
by A4, TARSKI:def 1;
then A15:
d in dom (<*f*> . 1)
by A14, Def3;
then
local_overlapping (
V,
A,
d,
(f . d),
v)
in dom p
by A1, Th26, A13, A3;
hence
a in dom (SC_Psuperpos (p,f,v))
by A5, A12, A3, A15;
verum
end;
let a be object ; ( not a in dom (SC_Psuperpos (p,f,v)) or (SC_Psuperpos (p,f,v)) . a = (SC_Psuperpos (p,x,<*v*>)) . a )
assume A16:
a in dom (SC_Psuperpos (p,f,v))
; (SC_Psuperpos (p,f,v)) . a = (SC_Psuperpos (p,x,<*v*>)) . a
then consider d being TypeSCNominativeData of V,A such that
A17:
d = a
and
local_overlapping (V,A,d,(f . d),v) in dom p
and
A18:
d in dom f
by A5;
NDentry (<*f*>,<*v*>,d) = naming (V,A,v,(f . d))
by A1, A18, Th26;
hence (SC_Psuperpos (p,x,<*v*>)) . a =
p . (local_overlapping (V,A,d,(f . d),v))
by A7, A16, A17, A2, Th33
.=
(SC_Psuperpos (p,f,v)) . a
by A16, A17, Th34
;
verum