for C1, C2 being Coherence_Space
for f, g being U-linear Function of C1,C2 st LinTrace f = LinTrace g holds
f = g