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 that
A1: a in union C1 and
A2: y in union C2 ; :: thesis: ex f being U-linear Function of C1,C2 st LinTrace f = {[a,y]}
[a,y] in [:(union C1),(union C2):] by A1, A2, ZFMISC_1:87;
then reconsider X = {[a,y]} as Subset of [:(union C1),(union C2):] by ZFMISC_1:31;
A3: now :: thesis: for a1, b being set st {a1,b} in C1 holds
for y1, y2 being object st [a1,y1] in X & [b,y2] in X holds
{y1,y2} in C2
let a1, b be set ; :: thesis: ( {a1,b} in C1 implies for y1, y2 being object st [a1,y1] in X & [b,y2] in X holds
{y1,y2} in C2 )
assume {a1,b} in C1 ; :: thesis: for y1, y2 being object st [a1,y1] in X & [b,y2] in X holds
{y1,y2} in C2
let y1, y2 be object ; :: thesis: ( [a1,y1] in X & [b,y2] in X implies {y1,y2} in C2 )
assume that
A4: [a1,y1] in X and
A5: [b,y2] in X ; :: thesis: {y1,y2} in C2
[b,y2] = [a,y] by A5, TARSKI:def 1;
then A6: y2 = y by XTUPLE_0:1;
[a1,y1] = [a,y] by A4, TARSKI:def 1;
then y1 = y by XTUPLE_0:1;
then {y1,y2} = {y} by A6, ENUMSET1:29;
hence {y1,y2} in C2 by A2, COH_SP:4; :: thesis: verum
end;
now :: thesis: for a1, b being set st {a1,b} in C1 holds
for y1 being object st [a1,y1] in X & [b,y1] in X holds
a1 = b
let a1, b be set ; :: thesis: ( {a1,b} in C1 implies for y1 being object st [a1,y1] in X & [b,y1] in X holds
a1 = b )
assume {a1,b} in C1 ; :: thesis: for y1 being object st [a1,y1] in X & [b,y1] in X holds
a1 = b
let y1 be object ; :: 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 XTUPLE_0:1; :: thesis: verum
end;
hence ex f being U-linear Function of C1,C2 st LinTrace f = {[a,y]} by A3, Th56; :: thesis: verum