let n be Nat; :: thesis: for S being RealNormSpace
for seq being Real_Sequence
for h being PartFunc of REAL, the carrier of S st rng seq c= dom h holds
seq . n in dom h
let S be RealNormSpace; :: thesis: for seq being Real_Sequence
for h being PartFunc of REAL, the carrier of S st rng seq c= dom h holds
seq . n in dom h
let seq be Real_Sequence; :: thesis: for h being PartFunc of REAL, the carrier of S st rng seq c= dom h holds
seq . n in dom h
let h be PartFunc of REAL, the carrier of S; :: thesis: ( rng seq c= dom h implies seq . n in dom h )
n in NAT by ORDINAL1:def 12;
then A1: n in dom seq by FUNCT_2:def 1;
assume rng seq c= dom h ; :: thesis: seq . n in dom h
then n in dom (h * seq) by A1, RELAT_1:27;
hence seq . n in dom h by FUNCT_1:11; :: thesis: verum