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

A2: now

let x be set ; :: thesis: ( x in X implies x `1 is finite )
assume x in X ; :: thesis: x `1 is finite
then x = [a,y] by TARSKI:def 1;
hence x `1 is finite by MCART_1:7; :: thesis: verum

end;

A3: now

let a1, b be Element of C1; :: 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 Element of C1; :: 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-stable Function of C1,C2 st Trace f = {[a,y]} by A2, A3, Th39; :: thesis: verum