let v be object ; :: thesis: for V, A being set
for d being TypeSCNominativeData of V,A
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A st d in dom (SC_Psuperpos (p,f,v)) holds
( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f )
let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A st d in dom (SC_Psuperpos (p,f,v)) holds
( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f )
let d be TypeSCNominativeData of V,A; :: thesis: for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A st d in dom (SC_Psuperpos (p,f,v)) holds
( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f )
let p be SCPartialNominativePredicate of V,A; :: thesis: for f being SCBinominativeFunction of V,A st d in dom (SC_Psuperpos (p,f,v)) holds
( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f )
let f be SCBinominativeFunction of V,A; :: thesis: ( d in dom (SC_Psuperpos (p,f,v)) implies ( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f ) )
set F = SC_Psuperpos (p,f,v);
assume A1: d in dom (SC_Psuperpos (p,f,v)) ; :: thesis: ( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f )
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;
then A2: ex d1 being TypeSCNominativeData of V,A st
( d1 = d & local_overlapping (V,A,d1,(f . d1),v) in dom p & d1 in dom f ) by A1;
then SC_Psuperpos (p,f,v),d =~ p, local_overlapping (V,A,d,(f . d),v) by Def11;
hence ( (SC_Psuperpos (p,f,v)) . d = p . (local_overlapping (V,A,d,(f . d),v)) & d in dom f ) by A2; :: thesis: verum