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 )
assume A1: graph f = graph g ; :: thesis: f = g
A2: ( dom f = C1 & 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 )
assume A4: graph f = graph g ; :: thesis: f . x c= g . x
A5: dom f = C1 by FUNCT_2:def 1;
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 A5, Th25;
hence z in g . x by A4, 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) )
assume A7: graph f = graph g ; :: thesis: f .: (Fin a) c= g .: (Fin a)
A8: ( dom f = C1 & dom g = C1 ) by FUNCT_2:def 1;
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
A9: ( x in dom f & x in Fin a & y = f . x ) by FUNCT_1:def 12;
( f . x c= g . x & g . x c= f . x ) by A3, A7, A9;
then f . x = g . x by XBOOLE_0:def 10;
hence y in g .: (Fin a) by A8, A9, FUNCT_1:def 12; :: thesis: verum

end;

end;

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 A1, A6;
then A10: f .: (Fin a) = g .: (Fin a) by XBOOLE_0:def 10;
thus f . a = union (f .: (Fin a)) by A2, Th21
.= g . a by A2, A10, Th21 ; :: thesis: verum

end;

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