let N be Element of NAT ; :: thesis: for seq being Real_Sequence of N holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0.REAL N )
let seq be Real_Sequence of N; :: thesis: ( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0.REAL N )
thus ( seq is non-zero implies for x being set st x in NAT holds
seq . x <> 0.REAL N ) :: thesis: ( ( for x being set st x in NAT holds
seq . x <> 0.REAL N ) implies seq is non-zero )

proof

assume seq is non-zero ; :: thesis: for x being set st x in NAT holds
seq . x <> 0.REAL N
then A1: rng seq c= the carrier of (TOP-REAL N) \ {(0.REAL N)} by Def1;
let x be set ; :: thesis: ( x in NAT implies seq . x <> 0.REAL N )
assume x in NAT ; :: thesis: seq . x <> 0.REAL N
then x in dom seq by Th2;
then seq . x in rng seq by FUNCT_1:def 5;
then not seq . x in {(0.REAL N)} by A1, XBOOLE_0:def 5;
hence seq . x <> 0.REAL N by TARSKI:def 1; :: thesis: verum

end;

assume A2: for x being set st x in NAT holds
seq . x <> 0.REAL N ; :: thesis: seq is non-zero

now

let y be set ; :: thesis: ( y in rng seq implies y in the carrier of (TOP-REAL N) \ {(0.REAL N)} )
assume y in rng seq ; :: thesis: y in the carrier of (TOP-REAL N) \ {(0.REAL N)}
then consider x being set such that
A3: x in dom seq and
A4: seq . x = y by FUNCT_1:def 5;
A5: x in NAT by A3, NORMSP_1:17;
then A6: y is Point of (TOP-REAL N) by A4, NORMSP_1:17;
y <> 0.REAL N by A2, A4, A5;
then not y in {(0.REAL N)} by TARSKI:def 1;
hence y in the carrier of (TOP-REAL N) \ {(0.REAL N)} by A6, XBOOLE_0:def 5; :: thesis: verum

end;

then rng seq c= the carrier of (TOP-REAL N) \ {(0.REAL N)} by TARSKI:def 3;
hence seq is non-zero by Def1; :: thesis: verum