let C1, C2 be Coherence_Space; :: thesis: 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
let f be U-linear Function of C1,C2; :: thesis: for X being Subset of (LinTrace f) ex g being U-linear Function of C1,C2 st LinTrace g = X
let X be Subset of (LinTrace f); :: thesis: ex g being U-linear Function of C1,C2 st LinTrace g = X
A1: X is Subset of [:(union C1),(union C2):] by XBOOLE_1:1;
A2: for a, b being set st {a,b} in C1 holds
for y1, y2 being set st [a,y1] in X & [b,y2] in X 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 X & [b,y] in X holds
a = b by Th55;
hence ex g being U-linear Function of C1,C2 st LinTrace g = X by A1, A2, Th57; :: thesis: verum