let V, A be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 <> {} ; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: ( 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; :: thesis: verum