environ
vocabularies HIDDEN, NUMBERS, RLVECT_1, STRUCT_0, SUBSET_1, ALGSTR_0, BINOP_1, FUNCT_1, ZFMISC_1, XBOOLE_0, REAL_1, PRE_TOPC, SUPINF_2, RLSUB_1, FUNCOP_1, CARD_1, RELAT_1, COMPLEX1, ARYTM_3, XXREAL_0, ARYTM_1, NAT_1, TARSKI, SEQ_2, ORDINAL2, NORMSP_1, NORMSP_0, RELAT_2, METRIC_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCOP_1, FUNCT_2, BINOP_1, RELAT_1, COMSEQ_2, SEQ_2, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, RLSUB_1, XXREAL_0, NORMSP_0;
definitions RLVECT_1, STRUCT_0, ALGSTR_0, NORMSP_0;
theorems TARSKI, NAT_1, FUNCT_1, SEQ_2, ABSVALUE, RLVECT_1, RLSUB_1, FUNCT_2, RELSET_1, XBOOLE_0, XCMPLX_0, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, ALGSTR_0, RELAT_1, NORMSP_0;
schemes FUNCT_2, NAT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, STRUCT_0, RLVECT_1, ALGSTR_0, NORMSP_0, XCMPLX_0, VALUED_0, NAT_1;
constructors HIDDEN, BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, SEQ_2, RLSUB_1, VALUED_1, RELSET_1, NORMSP_0, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RLVECT_1, STRUCT_0, ALGSTR_0, NORMSP_0;
expansions NORMSP_0;
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) --> (In (0,REAL)) as Function of the carrier of ((0). the RealLinearSpace),REAL ;
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) = |.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 ;