let v be object ; :: thesis: for V, A being set
for d being TypeSCNominativeData of V,A
for f, g being SCBinominativeFunction of V,A st d in dom (SC_Fsuperpos (f,g,v)) holds
( (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) & d in dom g )
let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for f, g being SCBinominativeFunction of V,A st d in dom (SC_Fsuperpos (f,g,v)) holds
( (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) & d in dom g )
let d be TypeSCNominativeData of V,A; :: thesis: for f, g being SCBinominativeFunction of V,A st d in dom (SC_Fsuperpos (f,g,v)) holds
( (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) & d in dom g )
let f, g be SCBinominativeFunction of V,A; :: thesis: ( d in dom (SC_Fsuperpos (f,g,v)) implies ( (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) & d in dom g ) )
set F = SC_Fsuperpos (f,g,v);
assume A1: d in dom (SC_Fsuperpos (f,g,v)) ; :: thesis: ( (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) & d in dom g )
dom (SC_Fsuperpos (f,g,v)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(g . d),v) in dom f & d in dom g ) } by Def15;
then A2: ex d1 being TypeSCNominativeData of V,A st
( d1 = d & local_overlapping (V,A,d1,(g . d1),v) in dom f & d1 in dom g ) by A1;
SC_Fsuperpos (f,g,v),d =~ f, local_overlapping (V,A,d,(g . d),v) by A2, Def15;
hence ( (SC_Fsuperpos (f,g,v)) . d = f . (local_overlapping (V,A,d,(g . d),v)) & d in dom g ) by A2; :: thesis: verum