for F being non empty Graph-yielding Function
for x being Element of dom F
for S being GraphSum of F ex M being PGraphMapping of F . x,S st M is strong_SG-embedding