begin
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
begin
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
Lm4:
now for V being ComplexLinearSpace
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * v
let V be
ComplexLinearSpace;
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet V1 be
Subset of
V;
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet D be non
empty set ;
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet d1 be
Element of
D;
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet A be
BinOp of
D;
for M being Function of [:COMPLEX,D:],D
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet M be
Function of
[:COMPLEX,D:],
D;
for z being Complex
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet z be
Complex;
for w being VECTOR of CLSStruct(# D,d1,A,M #)
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet w be
VECTOR of
CLSStruct(#
D,
d1,
A,
M #);
for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * vlet v be
Element of
V;
( V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v implies z * w = z * v )assume that A1:
V1 = D
and A2:
M = the
Mult of
V | [:COMPLEX,V1:]
and A3:
w = v
;
z * w = z * v
z in COMPLEX
by XCMPLX_0:def 2;
then
[z,w] in [:COMPLEX,V1:]
by A1, ZFMISC_1:def 2;
hence
z * w = z * v
by A3, A2, FUNCT_1:49;
verum
end;
Lm5:
for V being ComplexLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W
Lm6:
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 )
begin
deffunc H1( CNORMSTR ) -> Element of the carrier of $1 = 0. $1;
set V = the ComplexLinearSpace;
Lm7:
the carrier of ((0). the ComplexLinearSpace) = {(0. the ComplexLinearSpace)}
by Def9;
reconsider niltonil = the carrier of ((0). the ComplexLinearSpace) --> 0 as Function of the carrier of ((0). the ComplexLinearSpace),REAL by FUNCOP_1:45;
0. the ComplexLinearSpace is VECTOR of ((0). the ComplexLinearSpace)
by Lm7, TARSKI:def 1;
then Lm8:
niltonil . (0. the ComplexLinearSpace) = 0
by FUNCOP_1:7;
Lm9:
for u being VECTOR of ((0). the ComplexLinearSpace)
for z being Complex holds niltonil . (z * u) = |.z.| * (niltonil . u)
Lm10:
for u, v being VECTOR of ((0). the ComplexLinearSpace) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
reconsider X = CNORMSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),niltonil #) as non empty CNORMSTR ;