let S be RealNormSpace; :: thesis: for seq being sequence of S holds

( seq is non-zero iff for n being Nat holds seq . n <> 0. S )

let seq be sequence of S; :: thesis: ( seq is non-zero iff for n being Nat holds seq . n <> 0. S )

thus ( seq is non-zero implies for n being Nat holds seq . n <> 0. S ) by ORDINAL1:def 12, Th6; :: thesis: ( ( for n being Nat holds seq . n <> 0. S ) implies seq is non-zero )

assume for n being Nat holds seq . n <> 0. S ; :: thesis: seq is non-zero

then for x being set st x in NAT holds

seq . x <> 0. S ;

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

( seq is non-zero iff for n being Nat holds seq . n <> 0. S )

let seq be sequence of S; :: thesis: ( seq is non-zero iff for n being Nat holds seq . n <> 0. S )

thus ( seq is non-zero implies for n being Nat holds seq . n <> 0. S ) by ORDINAL1:def 12, Th6; :: thesis: ( ( for n being Nat holds seq . n <> 0. S ) implies seq is non-zero )

assume for n being Nat holds seq . n <> 0. S ; :: thesis: seq is non-zero

then for x being set st x in NAT holds

seq . x <> 0. S ;

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