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:87;
then reconsider X = {[a,y]} as Subset of [:C1,(union C2):] by ZFMISC_1:31;
A2: now :: thesis: for a1, b being Element of C1 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 Element of C1; :: 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
A3: [a1,y1] in X and
A4: [b,y2] in X ; :: thesis: {y1,y2} in C2
[b,y2] = [a,y] by A4, TARSKI:def 1;
then A5: y2 = y by XTUPLE_0:1;
[a1,y1] = [a,y] by A3, TARSKI:def 1;
then y1 = y by XTUPLE_0:1;
then {y1,y2} = {y} by A5, ENUMSET1:29;
hence {y1,y2} in C2 by A1, COH_SP:4; :: thesis: verum
end;
A6: now :: thesis: for a1, b being Element of C1 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 Element of C1; :: 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;
now :: thesis: for x being set st x in X holds
x `1 is finite
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 ; :: thesis: verum
end;
hence ex f being U-stable Function of C1,C2 st Trace f = {[a,y]} by A2, A6, Th38; :: thesis: verum