let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for X being Function
for f being SCBinominativeFunction of V,A
for g being V,A -FPrg-yielding FinSequence st product g <> {} holds
for x being Element of product g st d in dom (SC_Fsuperpos (f,x,X)) holds
( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
let d be TypeSCNominativeData of V,A; :: thesis: for X being Function
for f being SCBinominativeFunction of V,A
for g being V,A -FPrg-yielding FinSequence st product g <> {} holds
for x being Element of product g st d in dom (SC_Fsuperpos (f,x,X)) holds
( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
let X be Function; :: thesis: for f being SCBinominativeFunction of V,A
for g being V,A -FPrg-yielding FinSequence st product g <> {} holds
for x being Element of product g st d in dom (SC_Fsuperpos (f,x,X)) holds
( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
let f be SCBinominativeFunction of V,A; :: 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_Fsuperpos (f,x,X)) holds
( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (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_Fsuperpos (f,x,X)) holds
( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (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_Fsuperpos (f,x,X)) holds
( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
let x be Element of product g; :: thesis: ( d in dom (SC_Fsuperpos (f,x,X)) implies ( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) )
assume A2: d in dom (SC_Fsuperpos (f,x,X)) ; :: thesis: ( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) )
A3: dom ((SCFsuperpos (g,X)) . (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 ) } by A1, Def13;
SC_Fsuperpos (f,x,X) = (SCFsuperpos (g,X)) . (f,x) by A1, Def14;
then A4: ex d1 being TypeSCNominativeData of V,A st
( d1 = d & global_overlapping (V,A,d1,(NDentry (g,X,d1))) in dom f & d1 in_doms g ) by A2, A3;
then (SCFsuperpos (g,X)) . (f,x),d =~ f, global_overlapping (V,A,d,(NDentry (g,X,d))) by A1, Def13;
hence ( d in_doms g & (SC_Fsuperpos (f,x,X)) . d = f . (global_overlapping (V,A,d,(NDentry (g,X,d)))) ) by A1, A4, Def14; :: thesis: verum