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

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

let n be Element of NAT ; :: thesis: (1 (#) H) . n = H . n
thus (1 (#) H) . n = 1 (#) (H . n) by Def1
.= H . n by VFUNCT_1:18 ; :: thesis: verum

end;

hence 1 (#) H = H by FUNCT_2:63; :: thesis: verum