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 )

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

assume 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;

assume x in Lim s ; :: thesis: x in lim_f 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