let C1, C2 be Coherence_Space; ex f being U-stable Function of C1,C2 st Trace f = {}
reconsider X = {} as Subset of [:C1,(union C2):] by XBOOLE_1:2;
A1:
for a, b being Element of C1 st a \/ b in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b
;
( ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) )
;
hence
ex f being U-stable Function of C1,C2 st Trace f = {}
by A1, Th38; verum