let h be Function of T,(); :: thesis: ( h = f <--> g implies h is continuous )
assume A5: h = f <--> g ; :: thesis: h is continuous
A6: for r being Point of T holds h . r = (f . r) - (g . r)
proof
let r be Point of T; :: thesis: h . r = (f . r) - (g . r)
dom h = the carrier of T by FUNCT_2:def 1;
hence h . r = (f . r) - (g . r) by ; :: thesis: verum
end;
for p being Point of T
for V being Subset of () st h . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & h .: W c= V )
proof
let p be Point of T; :: thesis: for V being Subset of () st h . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & h .: W c= V )

let V be Subset of (); :: thesis: ( h . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & h .: W c= V ) )

assume ( h . p in V & V is open ) ; :: thesis: ex W being Subset of T st
( p in W & W is open & h .: W c= V )

then A7: h . p in Int V by TOPS_1:23;
reconsider r = h . p as Point of () by EUCLID:67;
consider r0 being Real such that
A8: ( r0 > 0 & Ball (r,r0) c= V ) by ;
reconsider r01 = f . p as Point of () by EUCLID:67;
reconsider G1 = Ball (r01,(r0 / 2)) as Subset of () by EUCLID:67;
A9: f . p in G1 by ;
A10: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
G1 is open by ;
then consider W1 being Subset of T such that
A11: ( p in W1 & W1 is open & f .: W1 c= G1 ) by ;
reconsider r02 = g . p as Point of () by EUCLID:67;
reconsider G2 = Ball (r02,(r0 / 2)) as Subset of () by EUCLID:67;
A12: g . p in G2 by ;
G2 is open by ;
then consider W2 being Subset of T such that
A13: ( p in W2 & W2 is open & g .: W2 c= G2 ) by ;
take W = W1 /\ W2; :: thesis: ( p in W & W is open & h .: W c= V )
thus p in W by ; :: thesis: ( W is open & h .: W c= V )
thus W is open by ; :: thesis: h .: W c= V
let x be Element of (); :: according to LATTICE7:def 1 :: thesis: ( not x in h .: W or x in V )
assume x in h .: W ; :: thesis: x in V
then consider z being object such that
A14: ( z in dom h & z in W & h . z = x ) by FUNCT_1:def 6;
A15: z in W1 by ;
reconsider pz = z as Point of T by A14;
dom f = the carrier of T by FUNCT_2:def 1;
then A16: f . pz in f .: W1 by ;
reconsider bb1 = f . pz as Point of () by EUCLID:67;
dist (r01,bb1) < r0 / 2 by ;
then A17: |.((f . p) - (f . pz)).| < r0 / 2 by JGRAPH_1:28;
A18: z in W2 by ;
dom g = the carrier of T by FUNCT_2:def 1;
then A19: g . pz in g .: W2 by ;
reconsider bb2 = g . pz as Point of () by EUCLID:67;
dist (r02,bb2) < r0 / 2 by ;
then A20: |.((g . p) - (g . pz)).| < r0 / 2 by JGRAPH_1:28;
A21: (f . pz) - (g . pz) = x by ;
reconsider bb0 = (f . pz) - (g . pz) as Point of () by EUCLID:67;
A22: h . pz = (f . pz) - (g . pz) by A6;
((f . p) - (g . p)) - ((f . pz) - (g . pz)) = (((f . p) - (g . p)) - (f . pz)) + (g . pz) by RLVECT_1:29
.= (((f . p) + (- (g . p))) + (- (f . pz))) + (g . pz)
.= (((f . p) + (- (f . pz))) + (- (g . p))) + (g . pz) by RLVECT_1:def 3
.= (((f . p) - (f . pz)) - (g . p)) + (g . pz)
.= (((f . p) - (f . pz)) + (g . pz)) + (- (g . p)) by RLVECT_1:def 3
.= ((f . p) - (f . pz)) + ((g . pz) - (g . p)) by RLVECT_1:def 3 ;
then A23: |.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| <= |.((f . p) - (f . pz)).| + |.((g . pz) - (g . p)).| by TOPRNS_1:29;
A24: |.((g . p) - (g . pz)).| = |.(- ((g . pz) - (g . p))).| by RLVECT_1:33
.= |.((g . pz) - (g . p)).| by TOPRNS_1:26 ;
|.((f . p) - (f . pz)).| + |.((g . p) - (g . pz)).| < (r0 / 2) + (r0 / 2) by ;
then |.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| < r0 by ;
then |.((h . p) - (h . pz)).| < r0 by ;
then dist (r,bb0) < r0 by ;
then x in Ball (r,r0) by ;
hence x in V by A8; :: thesis: verum
end;
hence h is continuous by JGRAPH_2:10; :: thesis: verum