for CNS1, CNS2 being ComplexNormSpace
for n being Nat
for seq being sequence of CNS1
for h being PartFunc of CNS1,CNS2 st rng seq c= dom h holds
seq . n in dom h