let S, T be non empty TopSpace; :: thesis:
let N be net of S; :: thesis:
A1: [#] T <> {} ;
let f be Function of S,T; :: thesis:
assume A2: f is continuous ; :: thesis:
let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: p in f .: (Lim N) ; :: thesis:
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:

let V be a_neighborhood of p; :: thesis:
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:

proof

take i9 ; :: according to WAYBEL_0:def 11 :: thesis:
let j9 be Element of (f * N); :: thesis:
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:
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:

end;

end;

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