let C1, C2 be Coherence_Space; :: thesis: for f, g being U-continuous Function of C1,C2 st graph f = graph g holds
f = g
let f, g be U-continuous Function of C1,C2; :: thesis: ( graph f = graph g implies f = g )
A1: dom f = C1 by FUNCT_2:def 1;
A2: dom g = C1 by FUNCT_2:def 1;

A3: now

let x be finite Element of C1; :: thesis: for f, g being U-continuous Function of C1,C2 st graph f = graph g holds
f . x c= g . x
let f, g be U-continuous Function of C1,C2; :: thesis: ( graph f = graph g implies f . x c= g . x )
A4: dom f = C1 by FUNCT_2:def 1;
assume A5: graph f = graph g ; :: thesis: f . x c= g . x
thus f . x c= g . x :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in f . x or z in g . x )
assume z in f . x ; :: thesis: z in g . x
then [x,z] in graph f by A4, Th25;
hence z in g . x by A5, Th25; :: thesis: verum

end;

end;

A6: now

let a be Element of C1; :: thesis: for f, g being U-continuous Function of C1,C2 st graph f = graph g holds
f .: (Fin a) c= g .: (Fin a)
let f, g be U-continuous Function of C1,C2; :: thesis: ( graph f = graph g implies f .: (Fin a) c= g .: (Fin a) )
A7: dom g = C1 by FUNCT_2:def 1;
assume A8: graph f = graph g ; :: thesis: f .: (Fin a) c= g .: (Fin a)
thus f .: (Fin a) c= g .: (Fin a) :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (Fin a) or y in g .: (Fin a) )
assume y in f .: (Fin a) ; :: thesis: y in g .: (Fin a)
then consider x being set such that
x in dom f and
A9: x in Fin a and
A10: y = f . x by FUNCT_1:def 12;
( f . x c= g . x & g . x c= f . x ) by A3, A8, A9;
then f . x = g . x by XBOOLE_0:def 10;
hence y in g .: (Fin a) by A7, A9, A10, FUNCT_1:def 12; :: thesis: verum

end;

end;

assume A11: graph f = graph g ; :: thesis: f = g

now

let a be Element of C1; :: thesis: f . a = g . a
( f .: (Fin a) c= g .: (Fin a) & g .: (Fin a) c= f .: (Fin a) ) by A11, A6;
then A12: f .: (Fin a) = g .: (Fin a) by XBOOLE_0:def 10;
thus f . a = union (f .: (Fin a)) by A1, Th21
.= g . a by A2, A12, Th21 ; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum