begin
:: deftheorem defines * CLVECT_1:def 1 :
:: deftheorem Def2 defines vector-distributive CLVECT_1:def 2 :
:: deftheorem Def3 defines scalar-distributive CLVECT_1:def 3 :
:: deftheorem Def4 defines scalar-associative CLVECT_1:def 4 :
:: deftheorem Def5 defines scalar-unital CLVECT_1:def 5 :
:: deftheorem defines Trivial-CLSStruct CLVECT_1:def 6 :
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem
theorem
Lm1:
for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V
Lm2:
for V being non empty addLoopStr
for F being FinSequence of the carrier of V st len F = 0 holds
Sum F = 0. V
theorem
theorem
theorem
theorem
theorem Th18:
theorem
theorem
begin
:: deftheorem Def7 defines linearly-closed CLVECT_1:def 7 :
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem
theorem
theorem
:: deftheorem Def8 defines Subspace CLVECT_1:def 8 :
theorem
theorem Th29:
theorem Th30:
theorem
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
Lm3:
for V being ComplexLinearSpace
for V1 being Subset of V
for W being Subspace of V st the carrier of W = V1 holds
V1 is linearly-closed
theorem Th37:
theorem
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem Th51:
theorem
theorem
theorem
theorem Th55:
:: deftheorem Def9 defines (0). CLVECT_1:def 9 :
:: deftheorem defines (Omega). CLVECT_1:def 10 :
theorem Th56:
theorem Th57:
theorem
theorem
theorem
theorem
:: deftheorem defines + CLVECT_1:def 11 :
Lm4:
for V being ComplexLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W
:: deftheorem Def12 defines Coset CLVECT_1:def 12 :
theorem Th62:
theorem Th63:
theorem
theorem Th65:
Lm5:
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
theorem Th66:
theorem Th67:
theorem
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem
theorem Th74:
theorem Th75:
theorem Th76:
theorem
theorem Th78:
theorem Th79:
theorem
theorem Th81:
theorem
theorem Th83:
theorem
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th98:
theorem
theorem
theorem
theorem
begin
deffunc H1( CNORMSTR ) -> Element of the carrier of $1 = 0. $1;
:: deftheorem defines ||. CLVECT_1:def 13 :
consider V being ComplexLinearSpace;
Lm6:
the carrier of ((0). V) = {(0. V)}
by Def9;
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 Lm6, TARSKI:def 1;
then Lm7:
niltonil . (0. V) = 0
by FUNCOP_1:13;
Lm8:
for u being VECTOR of ((0). V)
for z being Complex holds niltonil . (z * u) = |.z.| * (niltonil . u)
Lm9:
for u, v being VECTOR of ((0). V) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
reconsider X = CNORMSTR(# the carrier of ((0). V),(0. ((0). V)),the addF of ((0). V),the Mult of ((0). V),niltonil #) as non empty CNORMSTR ;
:: deftheorem Def14 defines ComplexNormSpace-like CLVECT_1:def 14 :
theorem
theorem Th104:
theorem Th105:
theorem Th106:
theorem
theorem Th108:
theorem Th109:
theorem Th110:
theorem Th111:
theorem Th112:
theorem
:: deftheorem Def15 defines * CLVECT_1:def 15 :
:: deftheorem Def16 defines convergent CLVECT_1:def 16 :
theorem
canceled;
theorem Th115:
theorem Th116:
theorem Th117:
theorem Th118:
:: deftheorem Def17 defines ||. CLVECT_1:def 17 :
theorem Th119:
:: deftheorem Def18 defines lim CLVECT_1:def 18 :
theorem
theorem
theorem
theorem
theorem