let X be RealUnitarySpace; :: thesis: for x being Point of X

for seq being sequence of X st seq is constant & ex n being Nat st seq . n = x holds

lim seq = x

let x be Point of X; :: thesis: for seq being sequence of X st seq is constant & ex n being Nat st seq . n = x holds

lim seq = x

let seq be sequence of X; :: thesis: ( seq is constant & ex n being Nat st seq . n = x implies lim seq = x )

assume that

A1: seq is constant and

A2: ex n being Nat st seq . n = x ; :: thesis: lim seq = x

consider n being Nat such that

A3: seq . n = x by A2;

n in NAT by ORDINAL1:def 12;

then n in dom seq by NORMSP_1:12;

then x in rng seq by A3, FUNCT_1:def 3;

hence lim seq = x by A1, Th10; :: thesis: verum

for seq being sequence of X st seq is constant & ex n being Nat st seq . n = x holds

lim seq = x

let x be Point of X; :: thesis: for seq being sequence of X st seq is constant & ex n being Nat st seq . n = x holds

lim seq = x

let seq be sequence of X; :: thesis: ( seq is constant & ex n being Nat st seq . n = x implies lim seq = x )

assume that

A1: seq is constant and

A2: ex n being Nat st seq . n = x ; :: thesis: lim seq = x

consider n being Nat such that

A3: seq . n = x by A2;

n in NAT by ORDINAL1:def 12;

then n in dom seq by NORMSP_1:12;

then x in rng seq by A3, FUNCT_1:def 3;

hence lim seq = x by A1, Th10; :: thesis: verum