let F be Function of T,R^1; :: thesis: ( F = f " implies F is continuous )

assume A1: F = f " ; :: thesis: F is continuous

dom f = the carrier of T by FUNCT_2:def 1;

then for q being Point of T holds f . q <> 0 ;

then consider g being Function of T,R^1 such that

A2: for p being Point of T

for r being Real st f . p = r holds

g . p = 1 / r and

A3: g is continuous by JGRAPH_2:26;

F = g

assume A1: F = f " ; :: thesis: F is continuous

dom f = the carrier of T by FUNCT_2:def 1;

then for q being Point of T holds f . q <> 0 ;

then consider g being Function of T,R^1 such that

A2: for p being Point of T

for r being Real st f . p = r holds

g . p = 1 / r and

A3: g is continuous by JGRAPH_2:26;

F = g

proof

hence
F is continuous
by A3; :: thesis: verum
let x be Point of T; :: according to FUNCT_2:def 8 :: thesis: F . x = g . x

thus F . x = 1 / (f . x) by A1, VALUED_1:10

.= g . x by A2 ; :: thesis: verum

end;thus F . x = 1 / (f . x) by A1, VALUED_1:10

.= g . x by A2 ; :: thesis: verum