let K1 be non empty Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = ((p `2 ) / (p `1 )) / (p `1 ) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q `1 <> 0 ) holds
f is continuous
let f be Function of ((TOP-REAL 2) | K1),R^1 ; :: thesis: ( ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = ((p `2 ) / (p `1 )) / (p `1 ) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q `1 <> 0 ) implies f is continuous )
assume A1: ( ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f . p = ((p `2 ) / (p `1 )) / (p `1 ) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q `1 <> 0 ) ) ; :: thesis: f is continuous
A2: the carrier of ((TOP-REAL 2) | K1) = [#] ((TOP-REAL 2) | K1)
.= K1 by PRE_TOPC:def 10 ;
reconsider g2 = proj2 | K1 as Function of ((TOP-REAL 2) | K1),R^1 by TOPMETR:24;
A3: for q being Point of ((TOP-REAL 2) | K1) holds g2 . q = proj2 . q

proof

let q be Point of ((TOP-REAL 2) | K1); :: thesis: g2 . q = proj2 . q
A4: q in the carrier of ((TOP-REAL 2) | K1) ;
dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then q in (dom proj2 ) /\ K1 by A2, A4, XBOOLE_0:def 4;
hence g2 . q = proj2 . q by FUNCT_1:71; :: thesis: verum

end;

then A5: g2 is continuous by Th40;
reconsider g1 = proj1 | K1 as Function of ((TOP-REAL 2) | K1),R^1 by TOPMETR:24;
A6: for q being Point of ((TOP-REAL 2) | K1) holds g1 . q = proj1 . q

proof

let q be Point of ((TOP-REAL 2) | K1); :: thesis: g1 . q = proj1 . q
A7: q in the carrier of ((TOP-REAL 2) | K1) ;
dom proj1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then q in (dom proj1 ) /\ K1 by A2, A7, XBOOLE_0:def 4;
hence g1 . q = proj1 . q by FUNCT_1:71; :: thesis: verum

end;

then A8: g1 is continuous by Th39;
for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0

proof

let q be Point of ((TOP-REAL 2) | K1); :: thesis: g1 . q <> 0
q in the carrier of ((TOP-REAL 2) | K1) ;
then reconsider q2 = q as Point of (TOP-REAL 2) by A2;
g1 . q = proj1 . q by A6
.= q2 `1 by PSCOMP_1:def 28 ;
hence g1 . q <> 0 by A1; :: thesis: verum

end;

then consider g3 being Function of ((TOP-REAL 2) | K1),R^1 such that
A9: ( ( for q being Point of ((TOP-REAL 2) | K1)
for r1, r2 being real number st g2 . q = r1 & g1 . q = r2 holds
g3 . q = (r1 / r2) / r2 ) & g3 is continuous ) by A5, A8, Th38;
dom g3 = the carrier of ((TOP-REAL 2) | K1) by FUNCT_2:def 1;
then A10: dom f = dom g3 by FUNCT_2:def 1;
for x being set st x in dom f holds
f . x = g3 . x

proof

let x be set ; :: thesis: ( x in dom f implies f . x = g3 . x )
assume A11: x in dom f ; :: thesis: f . x = g3 . x
then x in [#] ((TOP-REAL 2) | K1) ;
then x in K1 by PRE_TOPC:def 10;
then reconsider r = x as Point of (TOP-REAL 2) ;
reconsider s = x as Point of ((TOP-REAL 2) | K1) by A11;
A12: f . r = ((r `2 ) / (r `1 )) / (r `1 ) by A1, A11;
A13: g2 . s = proj2 . s by A3;
A14: g1 . s = proj1 . s by A6;
A15: proj2 . r = r `2 by PSCOMP_1:def 29;
proj1 . r = r `1 by PSCOMP_1:def 28;
hence f . x = g3 . x by A9, A12, A13, A14, A15; :: thesis: verum

end;

hence f is continuous by A9, A10, FUNCT_1:9; :: thesis: verum