let C1, C2 be Coherence_Space; :: thesis: ex f being U-linear Function of C1,C2 st LinTrace f = {}
reconsider X = {} as Subset of [:(union C1),(union C2):] by XBOOLE_1:2;
( ( for a, b being set 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 ) & ( for a, b being set st {a,b} in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b ) ) ;
hence ex f being U-linear Function of C1,C2 st LinTrace f = {} by Th56; :: thesis: verum