let C1, C2 be Coherence_Space; 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; for a being Element of C1 holds f . a = (Trace f) .: (Fin a)
let a be Element of C1; f . a = (Trace f) .: (Fin a)
set X = Trace f;
A1:
dom f = C1
by FUNCT_2:def 1;
( ( 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; verum