let seq be Real_Sequence; :: thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0 )
thus ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0 ) by Th6; :: thesis: ( ( for n being Element of NAT holds seq . n <> 0 ) implies seq is non-zero )
assume for n being Element of NAT holds seq . n <> 0 ; :: thesis: seq is non-zero
then for x being set st x in NAT holds
seq . x <> 0 ;
hence seq is non-zero by Th6; :: thesis: verum