let seq be Complex_Sequence; :: thesis: ( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0c )
thus ( seq is non-zero implies for x being set st x in NAT holds
seq . x <> 0c ) :: thesis: ( ( for x being set st x in NAT holds
seq . x <> 0c ) implies seq is non-zero )

proof

assume A1: seq is non-zero ; :: thesis: for x being set st x in NAT holds
seq . x <> 0c
let x be set ; :: thesis: ( x in NAT implies seq . x <> 0c )
assume x in NAT ; :: thesis: seq . x <> 0c
then x in dom seq by Th2;
then seq . x in rng seq by FUNCT_1:def 3;
hence seq . x <> 0c by A1; :: thesis: verum

end;

assume A2: for x being set st x in NAT holds
seq . x <> 0c ; :: thesis: seq is non-zero
assume 0 in rng seq ; :: according to ORDINAL1:def 15 :: thesis: contradiction
then 0 in rng seq ;
then ex x being object st
( x in dom seq & seq . x = 0 ) by FUNCT_1:def 3;
hence contradiction by A2; :: thesis: verum