let V, A be set ; for d being TypeSCNominativeData of V,A
for p being SCPartialNominativePredicate of V,A
for X being Function
for g being V,A -FPrg-yielding FinSequence st product g <> {} holds
for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds
( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
let d be TypeSCNominativeData of V,A; for p being SCPartialNominativePredicate of V,A
for X being Function
for g being V,A -FPrg-yielding FinSequence st product g <> {} holds
for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds
( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
let p be SCPartialNominativePredicate of V,A; for X being Function
for g being V,A -FPrg-yielding FinSequence st product g <> {} holds
for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds
( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
let X be Function; for g being V,A -FPrg-yielding FinSequence st product g <> {} holds
for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds
( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
let g be V,A -FPrg-yielding FinSequence; ( product g <> {} implies for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds
( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) )
assume A1:
product g <> {}
; for x being Element of product g st d in dom (SC_Psuperpos (p,x,X)) holds
( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
let x be Element of product g; ( d in dom (SC_Psuperpos (p,x,X)) implies ( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) )
assume A2:
d in dom (SC_Psuperpos (p,x,X))
; ( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
SC_Psuperpos (p,x,X) = (SCPsuperpos (g,X)) . (p,x)
by A1, Def10;
then
dom (SC_Psuperpos (p,x,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 ) }
by A1, Def9;
then A3:
ex d1 being TypeSCNominativeData of V,A st
( d1 = d & global_overlapping (V,A,d1,(NDentry (g,X,d1))) in dom p & d1 in_doms g )
by A2;
then
(SCPsuperpos (g,X)) . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d)))
by A1, Def9;
hence
( d in_doms g & (SC_Psuperpos (p,x,X)) . d = p . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
by A1, A3, Def10; verum