let f be real-valued FinSequence; :: thesis: ( |.f.| <> 0 implies ex i being Nat st

( i in dom f & f . i <> 0 ) )

assume |.f.| <> 0 ; :: thesis: ex i being Nat st

( i in dom f & f . i <> 0 )

then consider i being Element of NAT such that

A1: i in dom (sqr f) and

A2: (sqr f) . i <> 0 by PRVECT_2:3, SQUARE_1:17;

take i ; :: thesis: ( i in dom f & f . i <> 0 )

thus i in dom f by A1, VALUED_1:11; :: thesis: f . i <> 0

(sqr f) . i = (f . i) ^2 by VALUED_1:11;

hence f . i <> 0 by A2; :: thesis: verum

( i in dom f & f . i <> 0 ) )

assume |.f.| <> 0 ; :: thesis: ex i being Nat st

( i in dom f & f . i <> 0 )

then consider i being Element of NAT such that

A1: i in dom (sqr f) and

A2: (sqr f) . i <> 0 by PRVECT_2:3, SQUARE_1:17;

take i ; :: thesis: ( i in dom f & f . i <> 0 )

thus i in dom f by A1, VALUED_1:11; :: thesis: f . i <> 0

(sqr f) . i = (f . i) ^2 by VALUED_1:11;

hence f . i <> 0 by A2; :: thesis: verum