let v be object ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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*>; :: thesis: ( 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*> <> {} ; :: thesis: 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 S₁[ object ] means $1 in_doms <*f*>;
A3: <*f*> . 1 = f ;
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 & S₁[d] ) } by A2, Def9;
thus A7: dom (SC_Psuperpos (p,f,v)) = dom (SC_Psuperpos (p,x,<*v*>)) :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (SC_Psuperpos (p,f,v)) or (SC_Psuperpos (p,f,v)) . b₁ = (SC_Psuperpos (p,x,<*v*>)) . b₁ )

proof

thus dom (SC_Psuperpos (p,f,v)) c= dom (SC_Psuperpos (p,x,<*v*>)) :: according to XBOOLE_0:def 10 :: thesis: dom (SC_Psuperpos (p,x,<*v*>)) c= dom (SC_Psuperpos (p,f,v))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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)) ; :: thesis: 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: S₁[d]

proof

let x be object ; :: according to NOMIN_2:def 3 :: thesis: ( x in dom <*f*> implies d in dom (<*f*> . x) )
thus ( x in dom <*f*> implies d in dom (<*f*> . x) ) by A10, A3, A4, TARSKI:def 1; :: thesis: verum

end;

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; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( 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*>)) ; :: thesis: 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: S₁[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;
hence a in dom (SC_Psuperpos (p,f,v)) by A5, A12, A15; :: thesis: verum

end;

let a be object ; :: thesis: ( 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)) ; :: thesis: (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 ;
:: thesis: verum