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 :: thesis: for x being finite Element of C1
for f, g being U-continuous Function of C1,C2 st graph f = graph g holds
f . x c= g . x
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 object ; :: according to TARSKI:def 3 :: thesis: ( not z in f . x or z in g . x )
assume A6: z in f . x ; :: thesis: z in g . x
reconsider x = x, z = z as set by TARSKI:1;
[x,z] in graph f by A4, Th24, A6;
hence z in g . x by A5, Th24; :: thesis: verum
end;
end;
A7: now :: thesis: for a being Element of C1
for f, g being U-continuous Function of C1,C2 st graph f = graph g holds
f .: (Fin a) c= g .: (Fin a)
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) )
A8: dom g = C1 by FUNCT_2:def 1;
assume A9: 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 object ; :: 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 object such that
x in dom f and
A10: x in Fin a and
A11: y = f . x by FUNCT_1:def 6;
( f . x c= g . x & g . x c= f . x ) by A3, A9, A10;
then f . x = g . x ;
hence y in g .: (Fin a) by A8, A10, A11, FUNCT_1:def 6; :: thesis: verum
end;
end;
assume A12: graph f = graph g ; :: thesis: f = g
now :: thesis: for a being Element of C1 holds f . a = g . a
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 A12, A7;
then A13: f .: (Fin a) = g .: (Fin a) ;
thus f . a = union (f .: (Fin a)) by A1, Th20
.= g . a by A2, A13, Th20 ; :: thesis: verum
end;
hence f = g by FUNCT_2:63; :: thesis: verum