let C1, C2 be Coherence_Space; :: thesis: for A being set st ( for x, y being set st x in A & y in A holds
ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f ) holds
ex f being U-linear Function of C1,C2 st union A = LinTrace f
let A be set ; :: thesis: ( ( for x, y being set st x in A & y in A holds
ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f ) implies ex f being U-linear Function of C1,C2 st union A = LinTrace f )
assume A1: for x, y being set st x in A & y in A holds
ex f being U-linear Function of C1,C2 st x \/ y = LinTrace f ; :: thesis: ex f being U-linear Function of C1,C2 st union A = LinTrace f
set X = union A;

A2: now :: thesis: for a, b being set st {a,b} in C1 holds
for y1, y2 being object st [a,y1] in union A & [b,y2] in union A holds
{y1,y2} in C2

let a, b be set ; :: thesis: ( {a,b} in C1 implies for y1, y2 being object st [a,y1] in union A & [b,y2] in union A holds
{y1,y2} in C2 )
assume A3: {a,b} in C1 ; :: thesis: for y1, y2 being object st [a,y1] in union A & [b,y2] in union A holds
{y1,y2} in C2
let y1, y2 be object ; :: thesis: ( [a,y1] in union A & [b,y2] in union A implies {y1,y2} in C2 )
assume [a,y1] in union A ; :: thesis: ( [b,y2] in union A implies {y1,y2} in C2 )
then consider x1 being set such that
A4: [a,y1] in x1 and
A5: x1 in A by TARSKI:def 4;
assume [b,y2] in union A ; :: thesis: {y1,y2} in C2
then consider x2 being set such that
A6: [b,y2] in x2 and
A7: x2 in A by TARSKI:def 4;
A8: ( x1 c= x1 \/ x2 & x2 c= x1 \/ x2 ) by XBOOLE_1:7;
ex f being U-linear Function of C1,C2 st x1 \/ x2 = LinTrace f by A1, A5, A7;
hence {y1,y2} in C2 by A3, A4, A6, A8, Th53; :: thesis: verum

end;

A9: now :: thesis: for a, b being set st {a,b} in C1 holds
for y being object st [a,y] in union A & [b,y] in union A holds
a = b

let a, b be set ; :: thesis: ( {a,b} in C1 implies for y being object st [a,y] in union A & [b,y] in union A holds
a = b )
assume A10: {a,b} in C1 ; :: thesis: for y being object st [a,y] in union A & [b,y] in union A holds
a = b
let y be object ; :: thesis: ( [a,y] in union A & [b,y] in union A implies a = b )
assume [a,y] in union A ; :: thesis: ( [b,y] in union A implies a = b )
then consider x1 being set such that
A11: [a,y] in x1 and
A12: x1 in A by TARSKI:def 4;
assume [b,y] in union A ; :: thesis: a = b
then consider x2 being set such that
A13: [b,y] in x2 and
A14: x2 in A by TARSKI:def 4;
A15: ( x1 c= x1 \/ x2 & x2 c= x1 \/ x2 ) by XBOOLE_1:7;
ex f being U-linear Function of C1,C2 st x1 \/ x2 = LinTrace f by A1, A12, A14;
hence a = b by A10, A11, A13, A15, Th54; :: thesis: verum

end;

union A c= [:(union C1),(union C2):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union A or x in [:(union C1),(union C2):] )
assume x in union A ; :: thesis: x in [:(union C1),(union C2):]
then consider y being set such that
A16: x in y and
A17: y in A by TARSKI:def 4;
y \/ y = y ;
then ex f being U-linear Function of C1,C2 st y = LinTrace f by A1, A17;
hence x in [:(union C1),(union C2):] by A16; :: thesis: verum

end;

hence ex f being U-linear Function of C1,C2 st union A = LinTrace f by A2, A9, Th56; :: thesis: verum