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 ;
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 ;
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 :: thesis: for y being object st y in rng seq holds
y in NonZero S
let y be object ; :: thesis: ( y in rng seq implies y in NonZero S )
assume A3: y in rng seq ; :: thesis:
then ex x being object 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 ; :: thesis: verum
end;
then rng seq c= NonZero S ;
hence seq is non-zero ; :: thesis: verum