theorem Th61: :: COHSP_1:61

for C1, C2 being Coherence_Space
for f being U-linear Function of C1,C2
for X being Subset of (LinTrace f) ex g being U-linear Function of C1,C2 st LinTrace g = X