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