theorem :: COHSP_1:39
for C1, C2 being Coherence_Space
for f being U-stable Function of C1,C2
for a being Element of C1 holds f . a = (Trace f) .: (Fin a)