let M be non empty MetrSpace; :: thesis: for s being sequence of the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff x in Lim s )

let s be sequence of the carrier of (TopSpaceMetr M); :: thesis: for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff x in Lim s )

let x be Point of (TopSpaceMetr M); :: thesis: ( x in lim_f s iff x in Lim s )

then for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b by Th8;

hence x in lim_f s by Th6; :: thesis: verum

for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff x in Lim s )

let s be sequence of the carrier of (TopSpaceMetr M); :: thesis: for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff x in Lim s )

let x be Point of (TopSpaceMetr M); :: thesis: ( x in lim_f s iff x in Lim s )

hereby :: thesis: ( x in Lim s implies x in lim_f s )

assume
x in Lim s
; :: thesis: x in lim_f sassume
x in lim_f s
; :: thesis: x in Lim s

then for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b by Th6;

hence x in Lim s by Th8; :: thesis: verum

end;then for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b by Th6;

hence x in Lim s by Th8; :: thesis: verum

then for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b by Th8;

hence x in lim_f s by Th6; :: thesis: verum