for n being Nat
for S being RealNormSpace
for seq being Real_Sequence
for h being PartFunc of REAL, the carrier of S st rng seq c= dom h holds
seq . n in dom h