let N be Nat; :: thesis: for seq being Real_Sequence of N holds
( seq is non-zero iff for n being Nat holds seq . n <> 0. (TOP-REAL N) )
let seq be Real_Sequence of N; :: thesis: ( seq is non-zero iff for n being Nat holds seq . n <> 0. (TOP-REAL N) )
thus ( seq is non-zero implies for n being Nat holds seq . n <> 0. (TOP-REAL N) ) by ORDINAL1:def 12, Th2; :: thesis: ( ( for n being Nat holds seq . n <> 0. (TOP-REAL N) ) implies seq is non-zero )
assume for n being Nat holds seq . n <> 0. (TOP-REAL N) ; :: thesis: seq is non-zero
then for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) ;
hence seq is non-zero by Th2; :: thesis: verum