let T1, T2 be non empty TopSpace; for f being Function of T1,T2 st f is continuous holds
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; ( 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 )
assume A1:
f is continuous
; for S1 being sequence of T1
for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2
let S1 be sequence of T1; for S2 being sequence of T2 st S2 = f * S1 holds
f .: (Lim S1) c= Lim S2
let S2 be sequence of T2; ( S2 = f * S1 implies f .: (Lim S1) c= Lim S2 )
assume A2:
S2 = f * S1
; f .: (Lim S1) c= Lim S2
let y be object ; TARSKI:def 3 ( not y in f .: (Lim S1) or y in Lim S2 )
assume A3:
y in f .: (Lim S1)
; y in Lim S2
then reconsider y9 = y as Point of T2 ;
S2 is_convergent_to y9
proof
let U2 be
Subset of
T2;
FRECHET:def 3 ( not U2 is open or not y9 in U2 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or S2 . b2 in U2 ) )
assume that A4:
U2 is
open
and A5:
y9 in U2
;
ex b1 being set st
for b2 being set holds
( not b1 <= b2 or S2 . b2 in U2 )
consider x being
object such that A6:
x in dom f
and A7:
x in Lim S1
and A8:
y = f . x
by A3, FUNCT_1:def 6;
A9:
x in f " U2
by A5, A6, A8, FUNCT_1:def 7;
reconsider U1 =
f " U2 as
Subset of
T1 ;
[#] T2 <> {}
;
then A10:
U1 is
open
by A1, A4, TOPS_2:43;
reconsider x =
x as
Point of
T1 by A6;
S1 is_convergent_to x
by A7, FRECHET:def 5;
then consider n being
Nat such that A11:
for
m being
Nat st
n <= m holds
S1 . m in f " U2
by A10, A9;
take
n
;
for b1 being set holds
( not n <= b1 or S2 . b1 in U2 )
let m be
Nat;
( not n <= m or S2 . m in U2 )
A12:
m in NAT
by ORDINAL1:def 12;
assume
n <= m
;
S2 . m in U2
then
S1 . m in f " U2
by A11;
then A13:
f . (S1 . m) in U2
by FUNCT_1:def 7;
dom S1 = NAT
by FUNCT_2:def 1;
hence
S2 . m in U2
by A2, A13, FUNCT_1:13, A12;
verum
end;
hence
y in Lim S2
by FRECHET:def 5; verum