let C1, C2 be Coherence_Space; :: thesis: for X being Subset of [:(union C1),(union C2):] st ( for a, b being set st {a,b} in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being set st {a,b} in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b ) holds
ex f being U-linear Function of C1,C2 st X = LinTrace f
let X be Subset of [:(union C1),(union C2):]; :: thesis: ( ( for a, b being set st {a,b} in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being set st {a,b} in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b ) implies ex f being U-linear Function of C1,C2 st X = LinTrace f )
assume A1: ( ( for a, b being set st {a,b} in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being set st {a,b} in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b ) & ( for f being U-linear Function of C1,C2 holds not X = LinTrace f ) ) ; :: thesis: contradiction
then ex f being U-linear Function of C1,C2 st
( X = LinTrace f & ( for a being Element of C1 holds f . a = X .: a ) ) by Lm6;
hence contradiction by A1; :: thesis: verum