let X be RealUnitarySpace; :: thesis: for M being non empty Subset of X
for seq being sequence of X st rng seq c= the carrier of (Ort_Comp M) & seq is convergent holds
lim seq in the carrier of (Ort_Comp M)
let M be non empty Subset of X; :: thesis: for seq being sequence of X st rng seq c= the carrier of (Ort_Comp M) & seq is convergent holds
lim seq in the carrier of (Ort_Comp M)
let seq be sequence of X; :: thesis: ( rng seq c= the carrier of (Ort_Comp M) & seq is convergent implies lim seq in the carrier of (Ort_Comp M) )
assume that
A1: rng seq c= the carrier of (Ort_Comp M) and
A2: seq is convergent ; :: thesis: lim seq in the carrier of (Ort_Comp M)

now :: thesis: for x being Point of X st x in M holds
x .|. (lim seq) = 0

let x be Point of X; :: thesis: ( x in M implies x .|. (lim seq) = 0 )
assume A3: x in M ; :: thesis: x .|. (lim seq) = 0
defpred S₁[ Element of NAT , object ] means $2 = x .|. (seq . $1);
A4: for n being Element of NAT ex y being Element of REAL st S₁[n,y] ;
consider xseq being Function of NAT,REAL such that
A5: for n being Element of NAT holds S₁[n,xseq . n] from FUNCT_2:sch 3(A4);
reconsider xseq = xseq as Real_Sequence ;
A6: for i being Nat holds xseq . i = 0

proof

let i be Nat; :: thesis: xseq . i = 0
seq . i in rng seq by FUNCT_2:4, ORDINAL1:def 12;
then seq . i in the carrier of (Ort_Comp M) by A1;
then seq . i in Ort_CompSet M by Lm5;
then A7: x .|. (seq . i) = 0 by A3, Def1;
i in NAT by ORDINAL1:def 12;
hence xseq . i = 0 by A5, A7; :: thesis: verum

end;

for x, y being object st x in dom xseq & y in dom xseq holds
xseq . x = xseq . y

proof

let x, y be object ; :: thesis: ( x in dom xseq & y in dom xseq implies xseq . x = xseq . y )
assume ( x in dom xseq & y in dom xseq ) ; :: thesis: xseq . x = xseq . y
then reconsider i = x, j = y as Nat ;
thus xseq . x = xseq . i
.= 0 by A6
.= xseq . j by A6
.= xseq . y ; :: thesis: verum

end;

then A8: xseq is constant ;
then A10: lim xseq = xseq . 1 by SEQ_4:26
.= 0 by A6 ;
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((xseq . m) - (x .|. (lim seq))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((xseq . m) - (x .|. (lim seq))).| < p )
assume A11: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((xseq . m) - (x .|. (lim seq))).| < p
0 + 0 < ||.x.|| + 1 by XREAL_1:8, BHSP_1:28;
then consider n being Nat such that
A12: for m being Nat st n <= m holds
||.((seq . m) - (lim seq)).|| < p / (||.x.|| + 1) by A2, BHSP_2:19, A11;
take n ; :: thesis: for m being Nat st n <= m holds
|.((xseq . m) - (x .|. (lim seq))).| < p
let i be Nat; :: thesis: ( n <= i implies |.((xseq . i) - (x .|. (lim seq))).| < p )
assume n <= i ; :: thesis: |.((xseq . i) - (x .|. (lim seq))).| < p
then A13: ||.((seq . i) - (lim seq)).|| < p / (||.x.|| + 1) by A12;
|.((x .|. (seq . i)) - (x .|. (lim seq))).| = |.(x .|. ((seq . i) - (lim seq))).| by BHSP_1:12;
then A14: |.((x .|. (seq . i)) - (x .|. (lim seq))).| <= ||.x.|| * ||.((seq . i) - (lim seq)).|| by BHSP_1:29;
A15: ||.x.|| + 0 < ||.x.|| + 1 by XREAL_1:8;
0 <= ||.((seq . i) - (lim seq)).|| by BHSP_1:28;
then ||.x.|| * ||.((seq . i) - (lim seq)).|| <= (||.x.|| + 1) * ||.((seq . i) - (lim seq)).|| by XREAL_1:64, A15;
then A16: |.((x .|. (seq . i)) - (x .|. (lim seq))).| <= (||.x.|| + 1) * ||.((seq . i) - (lim seq)).|| by A14, XXREAL_0:2;
A17: 0 + 0 < ||.x.|| + 1 by XREAL_1:8, BHSP_1:28;
then ||.((seq . i) - (lim seq)).|| * (||.x.|| + 1) < (p / (||.x.|| + 1)) * (||.x.|| + 1) by A13, XREAL_1:68;
then ||.((seq . i) - (lim seq)).|| * (||.x.|| + 1) < p by A17, XCMPLX_1:87;
then A18: |.((x .|. (seq . i)) - (x .|. (lim seq))).| < p by A16, XXREAL_0:2;
i in NAT by ORDINAL1:def 12;
hence |.((xseq . i) - (x .|. (lim seq))).| < p by A18, A5; :: thesis: verum

end;

hence x .|. (lim seq) = 0 by A10, A8, SEQ_2:def 7; :: thesis: verum

end;

then lim seq in Ort_CompSet M by Def1;
hence lim seq in the carrier of (Ort_Comp M) by Lm5; :: thesis: verum