theorem Th5: :: NCFCONT1:5

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for n being Nat
for seq being sequence of CNS
for h being PartFunc of CNS,RNS st rng seq c= dom h holds
seq . n in dom h