theorem :: COHSP_1:60

for C1, C2 being Coherence_Space
for x, y being set st x in union C1 holds
for f being U-linear Function of C1,C2 st LinTrace f = {[x,y]} holds
for a being Element of C1 holds
( ( x in a implies f . a = {y} ) & ( not x in a implies f . a = {} ) )