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 )

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

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

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