let C1, C2 be Coherence_Space; :: thesis: for f being U-stable Function of C1,C2
for X being Subset of (Trace f) ex g being U-stable Function of C1,C2 st Trace g = X
let f be U-stable Function of C1,C2; :: thesis: for X being Subset of (Trace f) ex g being U-stable Function of C1,C2 st Trace g = X
let X be Subset of (Trace f); :: thesis: ex g being U-stable Function of C1,C2 st Trace g = X
A1: X is Subset of [:C1,(union C2):] by XBOOLE_1:1;

A2: now

let x be set ; :: thesis: ( x in X implies x `1 is finite )
assume A3: x in X ; :: thesis: x `1 is finite
then consider a, y being set such that
A4: ( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) by Def18;
dom f = C1 by FUNCT_2:def 1;
then a is finite by A3, A4, Th34;
hence x `1 is finite by A4, MCART_1:7; :: thesis: verum

end;

A5: for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being set st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 by Th35;
for a, b being Element of C1 st a \/ b in C1 holds
for y being set st [a,y] in X & [b,y] in X holds
a = b by Th36;
hence ex g being U-stable Function of C1,C2 st Trace g = X by A1, A2, A5, Th39; :: thesis: verum