let n be Nat; :: thesis: for S, T being RealNormSpace
for seq being sequence of S
for h being PartFunc of S,T st rng seq c= dom h holds
seq . n in dom h
let S, T be RealNormSpace; :: thesis: for seq being sequence of S
for h being PartFunc of S,T st rng seq c= dom h holds
seq . n in dom h
let seq be sequence of S; :: thesis: for h being PartFunc of S,T st rng seq c= dom h holds
seq . n in dom h
A1: n in NAT by ORDINAL1:def 12;
dom seq = NAT by FUNCT_2:def 1;
then seq . n in rng seq by FUNCT_1:def 3, A1;
hence for h being PartFunc of S,T st rng seq c= dom h holds
seq . n in dom h ; :: thesis: verum