begin
deffunc H1( NORMSTR ) -> Element of the carrier of $1 = 0. $1;
set V = the RealLinearSpace;
Lm1:
the carrier of ((0). the RealLinearSpace) = {(0. the RealLinearSpace)}
by RLSUB_1:def 3;
reconsider niltonil = the carrier of ((0). the RealLinearSpace) --> 0 as Function of the carrier of ((0). the RealLinearSpace),REAL by FUNCOP_1:45;
0. the RealLinearSpace is VECTOR of ((0). the RealLinearSpace)
by Lm1, TARSKI:def 1;
then Lm2:
niltonil . (0. the RealLinearSpace) = 0
by FUNCOP_1:7;
Lm3:
for u being VECTOR of ((0). the RealLinearSpace)
for a being Real holds niltonil . (a * u) = (abs a) * (niltonil . u)
Lm4:
for u, v being VECTOR of ((0). the RealLinearSpace) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
reconsider X = NORMSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),niltonil #) as non empty NORMSTR ;
Lm6:
for RNS being non empty 1-sorted
for S being sequence of RNS
for n being Element of NAT holds S . n is Element of RNS
;