begin
deffunc H1( NORMSTR ) -> Element of the carrier of $1 = 0. $1;
:: deftheorem defines ||. NORMSP_1:def 1 :
consider V being RealLinearSpace;
Lm1:
the carrier of ((0). V) = {(0. V)}
by RLSUB_1:def 3;
reconsider niltonil = the carrier of ((0). V) --> 0 as Function of the carrier of ((0). V),REAL by FUNCOP_1:57;
0. V is VECTOR of ((0). V)
by Lm1, TARSKI:def 1;
then Lm2:
niltonil . (0. V) = 0
by FUNCOP_1:13;
Lm3:
for u being VECTOR of ((0). V)
for a being Real holds niltonil . (a * u) = (abs a) * (niltonil . u)
Lm4:
for u, v being VECTOR of ((0). V) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
reconsider X = NORMSTR(# the carrier of ((0). V),(0. ((0). V)),the addF of ((0). V),the Mult of ((0). V),niltonil #) as non empty NORMSTR ;
:: deftheorem Def2 defines RealNormSpace-like NORMSP_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
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
;
:: deftheorem NORMSP_1:def 3 :
canceled;
:: deftheorem NORMSP_1:def 4 :
canceled;
:: deftheorem Def5 defines + NORMSP_1:def 5 :
:: deftheorem Def6 defines - NORMSP_1:def 6 :
:: deftheorem Def7 defines - NORMSP_1:def 7 :
:: deftheorem Def8 defines * NORMSP_1:def 8 :
:: deftheorem Def9 defines convergent NORMSP_1:def 9 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
:: deftheorem Def10 defines ||. NORMSP_1:def 10 :
theorem
canceled;
theorem Th39:
:: deftheorem Def11 defines lim NORMSP_1:def 11 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem