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

proof

assume seq is non-zero ; :: thesis: for x being set st x in NAT holds
seq . x <> 0. S
then A1: rng seq c= NonZero S by Def1;
let x be set ; :: thesis: ( x in NAT implies seq . x <> 0. S )
assume x in NAT ; :: thesis: seq . x <> 0. S
then x in dom seq by FUNCT_2:def 1;
then seq . x in rng seq by FUNCT_1:def 3;
then not seq . x in {(0. S)} by A1, XBOOLE_0:def 5;
hence seq . x <> 0. S by TARSKI:def 1; :: thesis: verum

end;

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

now

let y be set ; :: thesis: ( y in rng seq implies y in NonZero S )
assume A3: y in rng seq ; :: thesis: y in NonZero S
then ex x being set st
( x in dom seq & seq . x = y ) by FUNCT_1:def 3;
then y <> 0. S by A2;
then not y in {(0. S)} by TARSKI:def 1;
hence y in NonZero S by A3, XBOOLE_0:def 5; :: thesis: verum

end;

then rng seq c= NonZero S by TARSKI:def 3;
hence seq is non-zero by Def1; :: thesis: verum