let C1, C2 be Coherence_Space; :: thesis: for f being U-continuous Function of C1,C2
for a being Element of C1 holds f . a = (graph f) .: (Fin a)
let f be U-continuous Function of C1,C2; :: thesis: for a being Element of C1 holds f . a = (graph f) .: (Fin a)
let a be Element of C1; :: thesis: f . a = (graph f) .: (Fin a)
set X = graph f;
A1: now :: thesis: for x being set st x in graph f holds
x `1 is finite
let x be set ; :: thesis: ( x in graph f implies x `1 is finite )
assume x in graph f ; :: thesis: x `1 is finite
then ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) by Def16;
hence x `1 is finite ; :: thesis: verum
end;
dom f = C1 by FUNCT_2:def 1;
then A2: for a, b being finite Element of C1 st a c= b holds
for y being set st [a,y] in graph f holds
[b,y] in graph f by Th25;
for a being finite Element of C1
for y1, y2 being set st [a,y1] in graph f & [a,y2] in graph f holds
{y1,y2} in C2 by Th26;
then consider g being U-continuous Function of C1,C2 such that
A3: graph f = graph g and
A4: for a being Element of C1 holds g . a = (graph f) .: (Fin a) by A1, A2, Lm4;
g . a = (graph f) .: (Fin a) by A4;
hence f . a = (graph f) .: (Fin a) by A3, Th28; :: thesis: verum