let C1, C2 be Coherence_Space; for A being set st ( for x, y being set st x in A & y in A holds
ex f being U-stable Function of C1,C2 st x \/ y = Trace f ) holds
ex f being U-stable Function of C1,C2 st union A = Trace f
let A be set ; ( ( for x, y being set st x in A & y in A holds
ex f being U-stable Function of C1,C2 st x \/ y = Trace f ) implies ex f being U-stable Function of C1,C2 st union A = Trace f )
assume A1:
for x, y being set st x in A & y in A holds
ex f being U-stable Function of C1,C2 st x \/ y = Trace f
; ex f being U-stable Function of C1,C2 st union A = Trace f
set X = union A;
A2:
now for a, b being Element of C1 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 C2let a,
b be
Element of
C1;
( 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
;
for y1, y2 being object st [a,y1] in union A & [b,y2] in union A holds
{y1,y2} in C2let y1,
y2 be
object ;
( [a,y1] in union A & [b,y2] in union A implies {y1,y2} in C2 )assume
[a,y1] in union A
;
( [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
;
{y1,y2} in C2then 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-stable Function of
C1,
C2 st
x1 \/ x2 = Trace f
by A1, A5, A7;
hence
{y1,y2} in C2
by A3, A4, A6, A8, Th34;
verum end;
A9:
now for a, b being Element of C1 st a \/ b in C1 holds
for y being object st [a,y] in union A & [b,y] in union A holds
a = blet a,
b be
Element of
C1;
( 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
;
for y being object st [a,y] in union A & [b,y] in union A holds
a = blet y be
object ;
( [a,y] in union A & [b,y] in union A implies a = b )assume
[a,y] in union A
;
( [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
;
a = bthen 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-stable Function of
C1,
C2 st
x1 \/ x2 = Trace f
by A1, A12, A14;
hence
a = b
by A10, A11, A13, A15, Th35;
verum end;
union A c= [:C1,(union C2):]
hence
ex f being U-stable Function of C1,C2 st union A = Trace f
by A16, A2, A9, Th38; verum