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

proof

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

end;

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