let T1, T2 be non empty TopSpace; :: thesis: for f being Function of T1,T2 st f is continuous holds
for A being Subset of T1
for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is continuous
let f be Function of T1,T2; :: thesis: ( f is continuous implies for A being Subset of T1
for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is continuous )
assume A1: f is continuous ; :: thesis: for A being Subset of T1
for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is continuous
let A be Subset of T1; :: thesis: for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is continuous
let g be Function of (T1 | A),(T2 | (f .: A)); :: thesis: ( g = f | A implies g is continuous )
assume A2: g = f | A ; :: thesis: g is continuous
A3: ( [#] (T1 | A) = A & [#] (T2 | (f .: A)) = f .: A ) by PRE_TOPC:def 10;
A4: dom f = the carrier of T1 by FUNCT_2:def 1;

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: g is continuous

then ( T2 | (f .: A) is empty & T1 | A is empty ) by A3, RELAT_1:149;
hence g is continuous by TIETZE:6; :: thesis: verum

end;

suppose not A is empty ; :: thesis: g is continuous

then reconsider S1 = T1 | A, S2 = T2 | (f .: A) as non empty TopSpace by A4;
f | A = f | (T1 | A) by A3, TMAP_1:def 3;
then ( g is continuous Function of S1,T2 & g is Function of S1,S2 ) by A1, A2, TMAP_1:68;
hence g is continuous by JORDAN16:12; :: thesis: verum

end;

end;