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: dom f = the carrier of T1 by FUNCT_2:def 1;
A4: [#] (T1 | A) = A by PRE_TOPC:def 5;
per cases ( A is empty or not A is empty ) ;
suppose A is empty ; :: thesis: g is continuous
hence g is continuous by TIETZE:4; :: 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 A3;
f | A = f | (T1 | A) by A4, TMAP_1:def 3;
then A5: g is continuous Function of S1,T2 by A1, A2;
g is Function of S1,S2 ;
hence g is continuous by A5, JORDAN16:8; :: thesis: verum
end;
end;