let C1, C2 be Coherence_Space; :: thesis: for x, y being set st x in union C1 & y in union C2 holds
ex f being U-linear Function of C1,C2 st LinTrace f = {[x,y]}
let a, y be set ; :: thesis: ( a in union C1 & y in union C2 implies ex f being U-linear Function of C1,C2 st LinTrace f = {[a,y]} )
assume A1: ( a in union C1 & y in union C2 ) ; :: thesis: ex f being U-linear Function of C1,C2 st LinTrace f = {[a,y]}
then [a,y] in [:(union C1),(union C2):] by ZFMISC_1:106;
then reconsider X = {[a,y]} as Subset of [:(union C1),(union C2):] by ZFMISC_1:37;

A2: now

let a1, b be set ; :: thesis: ( {a1,b} in C1 implies for y1, y2 being set st [a1,y1] in X & [b,y2] in X holds
{y1,y2} in C2 )
assume {a1,b} in C1 ; :: thesis: for y1, y2 being set st [a1,y1] in X & [b,y2] in X holds
{y1,y2} in C2
let y1, y2 be set ; :: thesis: ( [a1,y1] in X & [b,y2] in X implies {y1,y2} in C2 )
assume ( [a1,y1] in X & [b,y2] in X ) ; :: thesis: {y1,y2} in C2
then ( [a1,y1] = [a,y] & [b,y2] = [a,y] ) by TARSKI:def 1;
then ( y1 = y & y2 = y ) by ZFMISC_1:33;
then {y1,y2} = {y} by ENUMSET1:69;
hence {y1,y2} in C2 by A1, COH_SP:4; :: thesis: verum

end;

now

let a1, b be set ; :: thesis: ( {a1,b} in C1 implies for y1 being set st [a1,y1] in X & [b,y1] in X holds
a1 = b )
assume {a1,b} in C1 ; :: thesis: for y1 being set st [a1,y1] in X & [b,y1] in X holds
a1 = b
let y1 be set ; :: thesis: ( [a1,y1] in X & [b,y1] in X implies a1 = b )
assume ( [a1,y1] in X & [b,y1] in X ) ; :: thesis: a1 = b
then ( [a1,y1] = [a,y] & [b,y1] = [a,y] ) by TARSKI:def 1;
hence a1 = b by ZFMISC_1:33; :: thesis: verum

end;

hence ex f being U-linear Function of C1,C2 st LinTrace f = {[a,y]} by A2, Th57; :: thesis: verum