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 )

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

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 A2:
for x being set st x in NAT holds
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;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

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