theorem Th6: :: NCFCONT1:6

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