let T1, T2 be non empty TopSpace; :: thesis: for f being Function of T1,T2 st T1 is sequential holds
( f is continuous iff for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 )
let f be Function of T1,T2; :: thesis: ( T1 is sequential implies ( f is continuous iff for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 ) )
assume A1: T1 is sequential ; :: thesis: ( f is continuous iff for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 )
thus ( f is continuous implies for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 ) by Th11; :: thesis: ( ( for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 ) implies f is continuous )
assume A2: for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2 ; :: thesis: f is continuous
let B be Subset of T2; :: according to PRE_TOPC:def 6 :: thesis: ( not B is closed or f " B is closed )
reconsider A = f " B as Subset of T1 ;
assume A3: B is closed ; :: thesis: f " B is closed
for S being sequence of T1 st S is convergent & rng S c= A holds
Lim S c= A
proof
reconsider B9 = B as Subset of T2 ;
let S be sequence of T1; :: thesis: ( S is convergent & rng S c= A implies Lim S c= A )
assume that
S is convergent and
A4: rng S c= A ; :: thesis: Lim S c= A
set S2 = f * S;
rng (f * S) c= B9
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (f * S) or z in B9 )
assume z in rng (f * S) ; :: thesis: z in B9
then consider n being object such that
A5: n in dom (f * S) and
A6: z = (f * S) . n by FUNCT_1:def 3;
dom S = NAT by NORMSP_1:12;
then S . n in rng S by A5, FUNCT_1:def 3;
then f . (S . n) in B by A4, FUNCT_1:def 7;
hence z in B9 by A5, A6, FUNCT_1:12; :: thesis: verum
end;
then A7: Lim (f * S) c= B9 by A3, Th9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim S or x in A )
A8: dom f = the carrier of T1 by FUNCT_2:def 1;
A9: f .: (Lim S) c= Lim (f * S) by A2;
assume A10: x in Lim S ; :: thesis: x in A
then f . x in f .: (Lim S) by A8, FUNCT_1:def 6;
then f . x in Lim (f * S) by A9;
hence x in A by A10, A8, A7, FUNCT_1:def 7; :: thesis: verum
end;
hence f " B is closed by A1; :: thesis: verum