let e be Real; :: thesis: ( 0< e implies ex N being Nat st for n being Nat st n >= N holds e <=(F1 # x). n ) assume 0< e
; :: thesis: ex N being Nat st for n being Nat st n >= N holds e <=(F1 # x). n then consider N being Nat such that A7:
for n being Nat for x being set st n >= N & x indom(F1 .0) holds |.(((F1 . n). x)-(f . x)).|< e
byA1; take N = N; :: thesis: for n being Nat st n >= N holds e <=(F1 # x). n