theorem :: COHSP_1:58

for C1, C2 being Coherence_Space ex f being U-linear Function of C1,C2 st LinTrace f = {}