let D be non empty set ; :: thesis: for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y holds ||.(r (#) H).|| = |.r.| (#) ||.H.||
let r be Real; :: thesis: for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y holds ||.(r (#) H).|| = |.r.| (#) ||.H.||
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y holds ||.(r (#) H).|| = |.r.| (#) ||.H.||
let H be Functional_Sequence of D, the carrier of Y; :: thesis: ||.(r (#) H).|| = |.r.| (#) ||.H.||

now :: thesis: for n being Element of NAT holds ||.(r (#) H).|| . n = (|.r.| (#) ||.H.||) . n

let n be Element of NAT ; :: thesis: ||.(r (#) H).|| . n = (|.r.| (#) ||.H.||) . n
thus ||.(r (#) H).|| . n = ||.((r (#) H) . n).|| by Def4
.= ||.(r (#) (H . n)).|| by Def1
.= |.r.| (#) ||.(H . n).|| by VFUNCT_1:22
.= |.r.| (#) (||.H.|| . n) by Def4
.= (|.r.| (#) ||.H.||) . n by SEQFUNC:def 1 ; :: thesis: verum

end;

hence ||.(r (#) H).|| = |.r.| (#) ||.H.|| by FUNCT_2:63; :: thesis: verum