let S, T be non empty TopSpace; :: thesis: for N being net of S
for f being Function of S,T st f is continuous holds
f .: (Lim N) c= Lim (f * N)
let N be net of S; :: thesis: for f being Function of S,T st f is continuous holds
f .: (Lim N) c= Lim (f * N)
A1: [#] T <> {} ;
let f be Function of S,T; :: thesis: ( f is continuous implies f .: (Lim N) c= Lim (f * N) )
assume A2: f is continuous ; :: thesis: f .: (Lim N) c= Lim (f * N)
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in f .: (Lim N) or p in Lim (f * N) )
assume A3: p in f .: (Lim N) ; :: thesis: p in Lim (f * N)
then reconsider p = p as Point of T ;
consider x being object such that
A4: x in the carrier of S and
A5: x in Lim N and
A6: p = f . x by A3, FUNCT_2:64;
reconsider x = x as Element of S by A4;

now :: thesis: for V being a_neighborhood of p holds f * N is_eventually_in V

let V be a_neighborhood of p; :: thesis: f * N is_eventually_in V
A7: p in Int V by CONNSP_2:def 1;
A8: x in f " (Int V) by A6, A7, FUNCT_2:38;
f " (Int V) is open by A1, A2, TOPS_2:43;
then f " (Int V) is a_neighborhood of x by A8, CONNSP_2:3;
then N is_eventually_in f " (Int V) by A5, YELLOW_6:def 15;
then consider i being Element of N such that
A9: for j being Element of N st j >= i holds
N . j in f " (Int V) ;
A10: the mapping of (f * N) = f * the mapping of N by WAYBEL_9:def 8;
A11: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def 8;
then reconsider i9 = i as Element of (f * N) ;
thus f * N is_eventually_in V :: thesis: verum

proof

take i9 ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (f * N) holds
( not i9 <= b₁ or (f * N) . b₁ in V )
let j9 be Element of (f * N); :: thesis: ( not i9 <= j9 or (f * N) . j9 in V )
reconsider j = j9 as Element of N by A11;
A12: f . (N . j) = (f * N) . j9 by A10, FUNCT_2:15;
assume j9 >= i9 ; :: thesis: (f * N) . j9 in V
then N . j in f " (Int V) by A9, A11, YELLOW_0:1;
then A13: f . (N . j) in Int V by FUNCT_2:38;
Int V c= V by TOPS_1:16;
hence (f * N) . j9 in V by A12, A13; :: thesis: verum

end;

end;

hence p in Lim (f * N) by YELLOW_6:def 15; :: thesis: verum