reconsider rj = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let P be non empty Subset of (TOP-REAL 2); :: thesis: for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds
ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Real
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = g . r ) )
let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: ( f is continuous implies ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Real
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = g . r ) ) )
assume A1: f is continuous ; :: thesis: ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Real
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = g . r ) )
reconsider f1 = f as Function ;
set h = (proj1 | P) * f;
A2: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 5;
then A3: rng f1 c= P by RELAT_1:def 19;
rj is continuous Function of (TOP-REAL 2),R^1 by Th10;
then rj | ((TOP-REAL 2) | P) is continuous Function of ((TOP-REAL 2) | P),R^1 ;
then rj | P is continuous Function of ((TOP-REAL 2) | P),R^1 by A2, TMAP_1:def 3;
then reconsider h2 = (proj1 | P) * f as continuous Function of I[01],R^1 by A1, Lm1;
take h2 ; :: thesis: ( h2 is continuous & ( for r being Real
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = h2 . r ) )
thus h2 is continuous ; :: thesis: for r being Real
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = h2 . r
let r be Real; :: thesis: for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = h2 . r
let q be Point of (TOP-REAL 2); :: thesis: ( r in the carrier of I[01] & q = f . r implies q `1 = h2 . r )
assume that
A4: r in the carrier of I[01] and
A5: q = f . r ; :: thesis: q `1 = h2 . r
A6: dom proj1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A7: r in dom f1 by A4, FUNCT_2:def 1;
then f1 . r in rng f1 by FUNCT_1:def 3;
then A8: q in (dom proj1) /\ P by A5, A3, A6, XBOOLE_0:def 4;
thus h2 . r = (proj1 | P) . q by A5, A7, FUNCT_1:13
.= proj1 . q by A8, FUNCT_1:48
.= q `1 by PSCOMP_1:def 5 ; :: thesis: verum