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 )

seq . x <> 0. S ; :: thesis: seq is non-zero

hence seq is non-zero ; :: thesis: verum

( 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 A2:
for x being set st x in NAT holds
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 A1, XBOOLE_0:def 5;

hence seq . x <> 0. S by TARSKI:def 1; :: thesis: verum

end;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 A1, XBOOLE_0:def 5;

hence seq . x <> 0. S by TARSKI:def 1; :: thesis: verum

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

then
rng seq c= NonZero S
;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: y in NonZero S

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 A3, XBOOLE_0:def 5; :: thesis: verum

end;assume A3: y in rng seq ; :: thesis: y in NonZero S

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 A3, XBOOLE_0:def 5; :: thesis: verum

hence seq is non-zero ; :: thesis: verum