let n be Element of NAT ; :: thesis: for CNS being ComplexNormSpace
for RNS being RealNormSpace
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
let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
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
let RNS be RealNormSpace; :: thesis: 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
let seq be sequence of CNS; :: thesis: for h being PartFunc of CNS,RNS st rng seq c= dom h holds
seq . n in dom h
let h be PartFunc of CNS,RNS; :: thesis: ( rng seq c= dom h implies seq . n in dom h )
assume A1: rng seq c= dom h ; :: thesis: seq . n in dom h
n in NAT ;
then n in dom seq by FUNCT_2:def 1;
then n in dom (h * seq) by A1, RELAT_1:46;
hence seq . n in dom h by FUNCT_1:21; :: thesis: verum