for C1, C2 being Coherence_Space
for a being finite Element of C1
for y being set st y in union C2 holds
ex f being U-stable Function of C1,C2 st Trace f = {[a,y]}