let seq be Complex_Sequence; :: thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0c )

thus ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0c ) by Th3; :: thesis: ( ( for n being Element of NAT holds seq . n <> 0c ) implies seq is non-zero )

assume for n being Element of NAT holds seq . n <> 0c ; :: thesis: seq is non-zero

then for x being set st x in NAT holds

seq . x <> 0c ;

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

thus ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0c ) by Th3; :: thesis: ( ( for n being Element of NAT holds seq . n <> 0c ) implies seq is non-zero )

assume for n being Element of NAT holds seq . n <> 0c ; :: thesis: seq is non-zero

then for x being set st x in NAT holds

seq . x <> 0c ;

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