let C1, C2 be Coherence_Space; :: thesis: for f being U-stable Function of C1,C2
for a being Element of C1 holds f . a = (Trace f) .: (Fin a)
let f be U-stable Function of C1,C2; :: thesis: for a being Element of C1 holds f . a = (Trace f) .: (Fin a)
let a be Element of C1; :: thesis: f . a = (Trace f) .: (Fin a)
set X = Trace f;
A1: dom f = C1 by FUNCT_2:def 1;
A2: now :: thesis: for x being set st x in Trace f holds
x `1 is finite
let x be set ; :: thesis: ( x in Trace f implies x `1 is finite )
assume A3: x in Trace f ; :: thesis: x `1 is finite
then consider a, y being set such that
A4: x = [a,y] and
a in dom f and
y in f . a and
for b being set st b in dom f & b c= a & y in f . b holds
a = b by Def17;
a is finite by A1, A3, A4, Th33;
hence x `1 is finite by A4; :: thesis: verum
end;
( ( for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being object st [a,y1] in Trace f & [b,y2] in Trace f holds
{y1,y2} in C2 ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y being object st [a,y] in Trace f & [b,y] in Trace f holds
a = b ) ) by Th34, Th35;
then consider g being U-stable Function of C1,C2 such that
A5: Trace f = Trace g and
A6: for a being Element of C1 holds g . a = (Trace f) .: (Fin a) by A2, Lm5;
g . a = (Trace f) .: (Fin a) by A6;
hence f . a = (Trace f) .: (Fin a) by A5, Th37; :: thesis: verum