let C1, C2 be Coherence_Space; :: thesis: for f being U-linear Function of C1,C2
for a being Element of C1 holds f . a = (LinTrace f) .: a
let f be U-linear Function of C1,C2; :: thesis: for a being Element of C1 holds f . a = (LinTrace f) .: a
let a be Element of C1; :: thesis: f . a = (LinTrace f) .: a
set X = LinTrace f;
A1: for a, b being set st {a,b} in C1 holds
for y1, y2 being set st [a,y1] in LinTrace f & [b,y2] in LinTrace f holds
{y1,y2} in C2 by Th54;
for a, b being set st {a,b} in C1 holds
for y being set st [a,y] in LinTrace f & [b,y] in LinTrace f holds
a = b by Th55;
then consider g being U-linear Function of C1,C2 such that
A2: ( LinTrace f = LinTrace g & ( for a being Element of C1 holds g . a = (LinTrace f) .: a ) ) by A1, Lm6;
g . a = (LinTrace f) .: a by A2;
hence f . a = (LinTrace f) .: a by A2, Th56; :: thesis: verum