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

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

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

then for x being object st x in NAT holds

seq . x <> 0 ;

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

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

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

then for x being object st x in NAT holds

seq . x <> 0 ;

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