let N be 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. (TOP-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. (TOP-REAL N) )
thus ( seq is non-zero implies for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) ) :: thesis: ( ( for x being set st x in NAT holds
seq . x <> 0. (TOP-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. (TOP-REAL N)
then A1: rng seq c= NonZero (TOP-REAL N) ;
let x be set ; :: thesis: ( x in NAT implies seq . x <> 0. (TOP-REAL N) )
assume x in NAT ; :: thesis: seq . x <> 0. (TOP-REAL N)
then x in dom seq by Th1;
then seq . x in rng seq by FUNCT_1:def 3;
then not seq . x in {(0. (TOP-REAL N))} by A1, XBOOLE_0:def 5;
hence seq . x <> 0. (TOP-REAL N) by TARSKI:def 1; :: thesis: verum

end;

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

now :: thesis: for y being object st y in rng seq holds
y in NonZero (TOP-REAL N)

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

end;

then rng seq c= NonZero (TOP-REAL N) by TARSKI:def 3;
hence seq is non-zero ; :: thesis: verum