let S1 be sequence of RealSpace; :: thesis: for seq being Real_Sequence
for g being Real
for g1 being Element of RealSpace st S1 = seq & g = g1 holds
( ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ) iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p )
let seq be Real_Sequence; :: thesis: for g being Real
for g1 being Element of RealSpace st S1 = seq & g = g1 holds
( ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ) iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p )
let g be Real; :: thesis: for g1 being Element of RealSpace st S1 = seq & g = g1 holds
( ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ) iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p )
let g1 be Element of RealSpace; :: thesis: ( S1 = seq & g = g1 implies ( ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ) iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p ) )
assume A1: ( S1 = seq & g = g1 ) ; :: thesis: ( ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ) iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p )

hereby :: thesis: ( ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p ) implies for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p )

assume A2: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ; :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p
thus for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p :: thesis: verum

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p
then consider n being Nat such that
A3: for m being Nat st n <= m holds
|.((seq . m) - g).| < p by A2;
A4: for m being Nat st n <= m holds
dist ((S1 . m),g1) < p

proof

let m be Nat; :: thesis: ( n <= m implies dist ((S1 . m),g1) < p )
assume C5: n <= m ; :: thesis: dist ((S1 . m),g1) < p
set s = seq . m;
set s1 = S1 . m;
dist ((S1 . m),g1) = |.((seq . m) - g).| by A1, TOPMETR:11;
hence dist ((S1 . m),g1) < p by A3, C5; :: thesis: verum

end;

take n ; :: thesis: for m being Nat st n <= m holds
dist ((S1 . m),g1) < p
thus for m being Nat st n <= m holds
dist ((S1 . m),g1) < p by A4; :: thesis: verum

end;

end;

assume A5: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p ; :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p
thus for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p :: thesis: verum

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p
then consider n being Nat such that
A6: for m being Nat st n <= m holds
dist ((S1 . m),g1) < p by A5;
A7: for m being Nat st n <= m holds
|.((seq . m) - g).| < p

proof

let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - g).| < p )
assume A8: n <= m ; :: thesis: |.((seq . m) - g).| < p
set s = seq . m;
set s1 = S1 . m;
dist ((S1 . m),g1) = |.((seq . m) - g).| by A1, TOPMETR:11;
hence |.((seq . m) - g).| < p by A6, A8; :: thesis: verum

end;

take n ; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - g).| < p
thus for m being Nat st n <= m holds
|.((seq . m) - g).| < p by A7; :: thesis: verum

end;