:: CLVECT_1 semantic presentation

begin

definition
attrc1 is strict ;
struct CLSStruct  ->  addLoopStr ;
aggrCLSStruct(# carrier, ZeroF, addF, Mult #) ->  CLSStruct ;
sel Mult c1 ->  Function of [:COMPLEX, the carrier of c1:], the carrier of c1;
end;

registration
cluster non empty for CLSStruct ;
existence
 not for b1 being CLSStruct holds b1 is empty
proof
set ZS = the non empty set ;
set O = the Element of the non empty set ;
set F = the BinOp of the non empty set ;
set G = the Function of [:COMPLEX, the non empty set :], the non empty set ;
take  CLSStruct(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set #) ; ::_thesis: not CLSStruct(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set #) is empty
thus  not the carrier of CLSStruct(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

definition
let V be CLSStruct ;
mode VECTOR of V is Element of V;
end;

definition
let V be non empty CLSStruct ;
let v be VECTOR of V;
let z be Complex;
funcz * v ->  Element of V equals :: CLVECT_1:def 1
 the Mult of V . [z,v];
coherence
 the Mult of V . [z,v] is Element of V
proof
reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2;
 the Mult of V . [z,v] is Element of V ;
hence  the Mult of V . [z,v] is Element of V ; ::_thesis: verum
end;
end;

:: deftheorem  defines * CLVECT_1:def_1_:_
 for V being non empty CLSStruct
for v being VECTOR of V
for z being Complex holds z * v = the Mult of V . [z,v];

registration
let ZS be non empty set ;
let O be Element of ZS;
let F be BinOp of ZS;
let G be Function of [:COMPLEX,ZS:],ZS;
cluster CLSStruct(# ZS,O,F,G #) ->  non empty ;
coherence
 not CLSStruct(# ZS,O,F,G #) is empty ;
end;


definition
let IT be non empty CLSStruct ;
attrIT is vector-distributive  means :Def2: :: CLVECT_1:def 2
 for a being Complex
for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w);
attrIT is scalar-distributive  means :Def3: :: CLVECT_1:def 3
 for a, b being Complex
for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v);
attrIT is scalar-associative  means :Def4: :: CLVECT_1:def 4
 for a, b being Complex
for v being VECTOR of IT holds (a * b) * v = a * (b * v);
attrIT is scalar-unital  means :Def5: :: CLVECT_1:def 5
 for v being VECTOR of IT holds 1r * v = v;
end;

:: deftheorem Def2 defines vector-distributive CLVECT_1:def_2_:_
 for IT being non empty CLSStruct holds
( IT is vector-distributive iff for a being Complex
for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w) );

:: deftheorem Def3 defines scalar-distributive CLVECT_1:def_3_:_
 for IT being non empty CLSStruct holds
( IT is scalar-distributive iff for a, b being Complex
for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v) );

:: deftheorem Def4 defines scalar-associative CLVECT_1:def_4_:_
 for IT being non empty CLSStruct holds
( IT is scalar-associative iff for a, b being Complex
for v being VECTOR of IT holds (a * b) * v = a * (b * v) );

:: deftheorem Def5 defines scalar-unital CLVECT_1:def_5_:_
 for IT being non empty CLSStruct holds
( IT is scalar-unital iff for v being VECTOR of IT holds 1r * v = v );

definition
func Trivial-CLSStruct  ->  strict CLSStruct  equals :: CLVECT_1:def 6
 CLSStruct(# 1,op0,op2,(pr2 (COMPLEX,1)) #);
coherence
 CLSStruct(# 1,op0,op2,(pr2 (COMPLEX,1)) #) is strict CLSStruct ;
end;

:: deftheorem  defines Trivial-CLSStruct CLVECT_1:def_6_:_
 Trivial-CLSStruct = CLSStruct(# 1,op0,op2,(pr2 (COMPLEX,1)) #);

registration
cluster Trivial-CLSStruct  -> 1 -element strict ;
coherence
 Trivial-CLSStruct is 1 -element
proof
 the carrier of Trivial-CLSStruct = {0} by CARD_1:49;
hence  the carrier of Trivial-CLSStruct is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for CLSStruct ;
existence
 ex b1 being non empty CLSStruct st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital )
proof
take S = Trivial-CLSStruct ; ::_thesis: ( S is strict & S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & S is vector-distributive & S is scalar-distributive & S is scalar-associative & S is scalar-unital )
thus  S is strict ; ::_thesis: ( S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable & S is vector-distributive & S is scalar-distributive & S is scalar-associative & S is scalar-unital )
thus  S is Abelian ::_thesis: ( S is add-associative & S is right_zeroed & S is right_complementable & S is vector-distributive & S is scalar-distributive & S is scalar-associative & S is scalar-unital )
proof
let x be Element of S; :: according to RLVECT_1:def_2 ::_thesis: for b1 being Element of the carrier of S holds x + b1 = b1 + x
thus  for b1 being Element of the carrier of S holds x + b1 = b1 + x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  S is add-associative ::_thesis: ( S is right_zeroed & S is right_complementable & S is vector-distributive & S is scalar-distributive & S is scalar-associative & S is scalar-unital )
proof
let x be Element of S; :: according to RLVECT_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of S holds (x + b1) + b2 = x + (b1 + b2)
thus  for b1, b2 being Element of the carrier of S holds (x + b1) + b2 = x + (b1 + b2) by STRUCT_0:def_10; ::_thesis: verum
end;
thus  S is right_zeroed ::_thesis: ( S is right_complementable & S is vector-distributive & S is scalar-distributive & S is scalar-associative & S is scalar-unital )
proof
let x be Element of S; :: according to RLVECT_1:def_4 ::_thesis: x + (0. S) = x
thus  x + (0. S) = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  S is right_complementable ::_thesis: ( S is vector-distributive & S is scalar-distributive & S is scalar-associative & S is scalar-unital )
proof
let x be Element of S; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
take  x ; :: according to ALGSTR_0:def_11 ::_thesis: x + x = 0. S
thus  x + x = 0. S by STRUCT_0:def_10; ::_thesis: verum
end;
thus  for a being Complex
for v, w being VECTOR of S holds a * (v + w) = (a * v) + (a * w) by STRUCT_0:def_10; :: according to CLVECT_1:def_2 ::_thesis: ( S is scalar-distributive & S is scalar-associative & S is scalar-unital )
thus  for a, b being Complex
for v being VECTOR of S holds (a + b) * v = (a * v) + (b * v) by STRUCT_0:def_10; :: according to CLVECT_1:def_3 ::_thesis: ( S is scalar-associative & S is scalar-unital )
thus  for a, b being Complex
for v being VECTOR of S holds (a * b) * v = a * (b * v) by STRUCT_0:def_10; :: according to CLVECT_1:def_4 ::_thesis: S is scalar-unital
thus  for v being VECTOR of S holds 1r * v = v by STRUCT_0:def_10; :: according to CLVECT_1:def_5 ::_thesis: verum
end;
end;

definition
mode ComplexLinearSpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ;
end;


theorem Th1: :: CLVECT_1:1
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex st ( z = 0 or v = 0. V ) holds
z * v = 0. V
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex st ( z = 0 or v = 0. V ) holds
z * v = 0. V
let v be VECTOR of V; ::_thesis: for z being Complex st ( z = 0 or v = 0. V ) holds
z * v = 0. V
let z be Complex; ::_thesis: ( ( z = 0 or v = 0. V ) implies z * v = 0. V )
assume A1: ( z = 0 or v = 0. V ) ; ::_thesis: z * v = 0. V
now__::_thesis:_z_*_v_=_0._V
percases ( z = 0c or v = 0. V ) by A1;
supposeA2: z = 0c ; ::_thesis: z * v = 0. V
v + (0c * v) = (1r * v) + (0c * v) by Def5
.= (1r + 0c) * v by Def3
.= v by Def5
.= v + (0. V) by RLVECT_1:4 ;
hence  z * v = 0. V by A2, RLVECT_1:8; ::_thesis: verum
end;
supposeA3: v = 0. V ; ::_thesis: z * v = 0. V
(z * (0. V)) + (z * (0. V)) = z * ((0. V) + (0. V)) by Def2
.= z * (0. V) by RLVECT_1:4
.= (z * (0. V)) + (0. V) by RLVECT_1:4 ;
hence  z * v = 0. V by A3, RLVECT_1:8; ::_thesis: verum
end;
end;
end;
hence  z * v = 0. V ; ::_thesis: verum
end;

theorem Th2: :: CLVECT_1:2
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds
( not z * v = 0. V or z = 0 or v = 0. V )
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex holds
( not z * v = 0. V or z = 0 or v = 0. V )
let v be VECTOR of V; ::_thesis: for z being Complex holds
( not z * v = 0. V or z = 0 or v = 0. V )
let z be Complex; ::_thesis: ( not z * v = 0. V or z = 0 or v = 0. V )
assume that
A1: z * v = 0. V and
A2: z <> 0 ; ::_thesis: v = 0. V
thus v = 1r * v by Def5
.= ((z ") * z) * v by A2, XCMPLX_0:def_7
.= (z ") * (0. V) by A1, Def4
.= 0. V by Th1 ; ::_thesis: verum
end;

theorem Th3: :: CLVECT_1:3
for V being ComplexLinearSpace
for v being VECTOR of V holds - v = (- 1r) * v
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V holds - v = (- 1r) * v
let v be VECTOR of V; ::_thesis: - v = (- 1r) * v
v + ((- 1r) * v) = (1r * v) + ((- 1r) * v) by Def5
.= (1r + (- 1r)) * v by Def3
.= 0. V by Th1 ;
hence  - v = (- v) + (v + ((- 1r) * v)) by RLVECT_1:4
.= ((- v) + v) + ((- 1r) * v) by RLVECT_1:def_3
.= (0. V) + ((- 1r) * v) by RLVECT_1:5
.= (- 1r) * v by RLVECT_1:4 ;
::_thesis: verum
end;

theorem Th4: :: CLVECT_1:4
for V being ComplexLinearSpace
for v being VECTOR of V st v = - v holds
v = 0. V
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V st v = - v holds
v = 0. V
let v be VECTOR of V; ::_thesis: ( v = - v implies v = 0. V )
assume  v = - v ; ::_thesis: v = 0. V
then  0. V = v - (- v) by RLVECT_1:15
.= v + v by RLVECT_1:17
.= (1r * v) + v by Def5
.= (1r * v) + (1r * v) by Def5
.= (1r + 1r) * v by Def3 ;
hence  v = 0. V by Th2; ::_thesis: verum
end;

theorem :: CLVECT_1:5
for V being ComplexLinearSpace
for v being VECTOR of V st v + v = 0. V holds
v = 0. V
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V st v + v = 0. V holds
v = 0. V
let v be VECTOR of V; ::_thesis: ( v + v = 0. V implies v = 0. V )
assume  v + v = 0. V ; ::_thesis: v = 0. V
then  v = - v by RLVECT_1:def_10;
hence  v = 0. V by Th4; ::_thesis: verum
end;

theorem Th6: :: CLVECT_1:6
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds z * (- v) = (- z) * v
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex holds z * (- v) = (- z) * v
let v be VECTOR of V; ::_thesis: for z being Complex holds z * (- v) = (- z) * v
let z be Complex; ::_thesis: z * (- v) = (- z) * v
thus z * (- v) = z * ((- 1r) * v) by Th3
.= (z * (- 1r)) * v by Def4
.= (- z) * v ; ::_thesis: verum
end;

theorem Th7: :: CLVECT_1:7
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds z * (- v) = - (z * v)
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex holds z * (- v) = - (z * v)
let v be VECTOR of V; ::_thesis: for z being Complex holds z * (- v) = - (z * v)
let z be Complex; ::_thesis: z * (- v) = - (z * v)
thus z * (- v) = (- (1r * z)) * v by Th6
.= ((- 1r) * z) * v
.= (- 1r) * (z * v) by Def4
.= - (z * v) by Th3 ; ::_thesis: verum
end;

theorem :: CLVECT_1:8
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex holds (- z) * (- v) = z * v
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex holds (- z) * (- v) = z * v
let v be VECTOR of V; ::_thesis: for z being Complex holds (- z) * (- v) = z * v
let z be Complex; ::_thesis: (- z) * (- v) = z * v
thus (- z) * (- v) = (- (- z)) * v by Th6
.= z * v ; ::_thesis: verum
end;

theorem Th9: :: CLVECT_1:9
for V being ComplexLinearSpace
for v, u being VECTOR of V
for z being Complex holds z * (v - u) = (z * v) - (z * u)
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for z being Complex holds z * (v - u) = (z * v) - (z * u)
let v, u be VECTOR of V; ::_thesis: for z being Complex holds z * (v - u) = (z * v) - (z * u)
let z be Complex; ::_thesis: z * (v - u) = (z * v) - (z * u)
thus z * (v - u) = (z * v) + (z * (- u)) by Def2
.= (z * v) - (z * u) by Th7 ; ::_thesis: verum
end;

theorem Th10: :: CLVECT_1:10
for V being ComplexLinearSpace
for v being VECTOR of V
for z1, z2 being Complex holds (z1 - z2) * v = (z1 * v) - (z2 * v)
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z1, z2 being Complex holds (z1 - z2) * v = (z1 * v) - (z2 * v)
let v be VECTOR of V; ::_thesis: for z1, z2 being Complex holds (z1 - z2) * v = (z1 * v) - (z2 * v)
let z1, z2 be Complex; ::_thesis: (z1 - z2) * v = (z1 * v) - (z2 * v)
thus (z1 - z2) * v = (z1 + (- z2)) * v
.= (z1 * v) + ((- z2) * v) by Def3
.= (z1 * v) + (z2 * (- v)) by Th6
.= (z1 * v) - (z2 * v) by Th7 ; ::_thesis: verum
end;

theorem :: CLVECT_1:11
for V being ComplexLinearSpace
for v, u being VECTOR of V
for z being Complex st z <> 0 & z * v = z * u holds
v = u
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for z being Complex st z <> 0 & z * v = z * u holds
v = u
let v, u be VECTOR of V; ::_thesis: for z being Complex st z <> 0 & z * v = z * u holds
v = u
let z be Complex; ::_thesis: ( z <> 0 & z * v = z * u implies v = u )
assume that
A1: z <> 0 and
A2: z * v = z * u ; ::_thesis: v = u
0. V = (z * v) - (z * u) by A2, RLVECT_1:15
.= z * (v - u) by Th9 ;
then  v - u = 0. V by A1, Th2;
hence  v = u by RLVECT_1:21; ::_thesis: verum
end;

theorem :: CLVECT_1:12
for V being ComplexLinearSpace
for v being VECTOR of V
for z1, z2 being Complex st v <> 0. V & z1 * v = z2 * v holds
z1 = z2
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z1, z2 being Complex st v <> 0. V & z1 * v = z2 * v holds
z1 = z2
let v be VECTOR of V; ::_thesis: for z1, z2 being Complex st v <> 0. V & z1 * v = z2 * v holds
z1 = z2
let z1, z2 be Complex; ::_thesis: ( v <> 0. V & z1 * v = z2 * v implies z1 = z2 )
assume that
A1: v <> 0. V and
A2: z1 * v = z2 * v ; ::_thesis: z1 = z2
0. V = (z1 * v) - (z2 * v) by A2, RLVECT_1:15
.= (z1 - z2) * v by Th10 ;
then  (- z2) + z1 = 0 by A1, Th2;
hence  z1 = z2 ; ::_thesis: verum
end;

Lm1:  for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V
proof
let V be non empty addLoopStr ; ::_thesis: Sum (<*> the carrier of V) = 0. V
set S = <*> the carrier of V;
 ex f being Function of NAT, the carrier of V st
( Sum (<*> the carrier of V) = f . (len (<*> the carrier of V)) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len (<*> the carrier of V) & v = (<*> the carrier of V) . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def_12;
hence  Sum (<*> the carrier of V) = 0. V ; ::_thesis: verum
end;

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
proof
let V be non empty addLoopStr ; ::_thesis: for F being FinSequence of the carrier of V st len F = 0 holds
Sum F = 0. V
let F be FinSequence of the carrier of V; ::_thesis: ( len F = 0 implies Sum F = 0. V )
assume  len F = 0 ; ::_thesis: Sum F = 0. V
then  F = <*> the carrier of V ;
hence  Sum F = 0. V by Lm1; ::_thesis: verum
end;

theorem :: CLVECT_1:13
for V being ComplexLinearSpace
for z being Complex
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) holds
Sum F = z * (Sum G)
proof
let V be ComplexLinearSpace; ::_thesis: for z being Complex
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) holds
Sum F = z * (Sum G)
let z be Complex; ::_thesis: for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) holds
Sum F = z * (Sum G)
let F, G be FinSequence of the carrier of V; ::_thesis: ( len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) implies Sum F = z * (Sum G) )
defpred S1[ set ] means  for H, I being FinSequence of the carrier of V st len H = len I & len H = $1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I);
A1: dom F = Seg (len F) by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_st_(_for_H,_I_being_FinSequence_of_the_carrier_of_V_st_len_H_=_len_I_&_len_H_=_n_&_(_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_Seg_(len_H)_&_v_=_I_._k_holds_
H_._k_=_z_*_v_)_holds_
Sum_H_=_z_*_(Sum_I)_)_holds_
for_H,_I_being_FinSequence_of_the_carrier_of_V_st_len_H_=_len_I_&_len_H_=_n_+_1_&_(_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_Seg_(len_H)_&_v_=_I_._k_holds_
H_._k_=_z_*_v_)_holds_
Sum_H_=_z_*_(Sum_I)
let n be Element of NAT ; ::_thesis: ( ( for H, I being FinSequence of the carrier of V st len H = len I & len H = n & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I) ) implies for H, I being FinSequence of the carrier of V st len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I) )
assume A2: for H, I being FinSequence of the carrier of V st len H = len I & len H = n & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I) ; ::_thesis: for H, I being FinSequence of the carrier of V st len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I)
let H, I be FinSequence of the carrier of V; ::_thesis: ( len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) implies Sum H = z * (Sum I) )
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ; ::_thesis: Sum H = z * (Sum I)
reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of the carrier of V by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then A7: len q = n by A3, A4, FINSEQ_1:17;
A8: len p = n by A4, A6, FINSEQ_1:17;
A9: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_Seg_(len_p)_&_v_=_q_._k_holds_
p_._k_=_z_*_v
 len p <= len H by A4, A6, FINSEQ_1:17;
then A10: Seg (len p) c= Seg (len H) by FINSEQ_1:5;
A11: dom p = Seg n by A4, A6, FINSEQ_1:17;
let k be Element of NAT ; ::_thesis: for v being VECTOR of V st k in Seg (len p) & v = q . k holds
p . k = z * v
let v be VECTOR of V; ::_thesis: ( k in Seg (len p) & v = q . k implies p . k = z * v )
assume that
A12: k in Seg (len p) and
A13: v = q . k ; ::_thesis: p . k = z * v
 dom q = Seg n by A3, A4, A6, FINSEQ_1:17;
then  I . k = q . k by A8, A12, FUNCT_1:47;
then  H . k = z * v by A5, A12, A13, A10;
hence  p . k = z * v by A8, A12, A11, FUNCT_1:47; ::_thesis: verum
end;
 n + 1 in Seg (n + 1) by FINSEQ_1:4;
then  ( n + 1 in dom H & n + 1 in dom I ) by A3, A4, FINSEQ_1:def_3;
then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as VECTOR of V by FUNCT_1:102;
A14: v1 = z * v2 by A4, A5, FINSEQ_1:4;
A15: dom q = Seg (len q) by FINSEQ_1:def_3;
 dom p = Seg (len p) by FINSEQ_1:def_3;
hence  Sum H = (Sum p) + v1 by A4, A8, RLVECT_1:38
.= (z * (Sum q)) + (z * v2) by A2, A8, A7, A9, A14
.= z * ((Sum q) + v2) by Def2
.= z * (Sum I) by A3, A4, A7, A15, RLVECT_1:38 ;
::_thesis: verum
end;
then A16: for n being Element of NAT st S1[n] holds
S1[n + 1] ;
now__::_thesis:_for_H,_I_being_FinSequence_of_the_carrier_of_V_st_len_H_=_len_I_&_len_H_=_0_&_(_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_Seg_(len_H)_&_v_=_I_._k_holds_
H_._k_=_z_*_v_)_holds_
Sum_H_=_z_*_(Sum_I)
let H, I be FinSequence of the carrier of V; ::_thesis: ( len H = len I & len H = 0 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) implies Sum H = z * (Sum I) )
assume that
A17: len H = len I and
A18: len H = 0 and
 for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ; ::_thesis: Sum H = z * (Sum I)
 Sum H = 0. V by A18, Lm2;
hence  Sum H = z * (Sum I) by A17, A18, Lm2, Th1; ::_thesis: verum
end;
then A19: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A19, A16);
hence  ( len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) implies Sum F = z * (Sum G) ) by A1; ::_thesis: verum
end;

theorem :: CLVECT_1:14
for V being ComplexLinearSpace
for z being Complex holds z * (Sum (<*> the carrier of V)) = 0. V by Lm1, Th1;

theorem :: CLVECT_1:15
for V being ComplexLinearSpace
for v, u being VECTOR of V
for z being Complex holds z * (Sum <*v,u*>) = (z * v) + (z * u)
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for z being Complex holds z * (Sum <*v,u*>) = (z * v) + (z * u)
let v, u be VECTOR of V; ::_thesis: for z being Complex holds z * (Sum <*v,u*>) = (z * v) + (z * u)
let z be Complex; ::_thesis: z * (Sum <*v,u*>) = (z * v) + (z * u)
thus z * (Sum <*v,u*>) = z * (v + u) by RLVECT_1:45
.= (z * v) + (z * u) by Def2 ; ::_thesis: verum
end;

theorem :: CLVECT_1:16
for V being ComplexLinearSpace
for u, v1, v2 being VECTOR of V
for z being Complex holds z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)
proof
let V be ComplexLinearSpace; ::_thesis: for u, v1, v2 being VECTOR of V
for z being Complex holds z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)
let u, v1, v2 be VECTOR of V; ::_thesis: for z being Complex holds z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)
let z be Complex; ::_thesis: z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)
thus z * (Sum <*u,v1,v2*>) = z * ((u + v1) + v2) by RLVECT_1:46
.= (z * (u + v1)) + (z * v2) by Def2
.= ((z * u) + (z * v1)) + (z * v2) by Def2 ; ::_thesis: verum
end;

theorem Th17: :: CLVECT_1:17
for V being ComplexLinearSpace
for v being VECTOR of V holds Sum <*v,v*> = (1r + 1r) * v
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V holds Sum <*v,v*> = (1r + 1r) * v
let v be VECTOR of V; ::_thesis: Sum <*v,v*> = (1r + 1r) * v
thus  Sum <*v,v*> = v + v by RLVECT_1:45
.= (1r * v) + v by Def5
.= (1r * v) + (1r * v) by Def5
.= (1r + 1r) * v by Def3 ; ::_thesis: verum
end;

theorem :: CLVECT_1:18
for V being ComplexLinearSpace
for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- (1r + 1r)) * v
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- (1r + 1r)) * v
let v be VECTOR of V; ::_thesis: Sum <*(- v),(- v)*> = (- (1r + 1r)) * v
reconsider 2r = 2 + (0 * <i>) as Element of COMPLEX by XCMPLX_0:def_2;
thus  Sum <*(- v),(- v)*> = - (v + v) by RLVECT_1:60
.= - (Sum <*v,v*>) by RLVECT_1:45
.= - ((1r + 1r) * v) by Th17
.= (- 1r) * (2r * v) by Th3
.= ((- 1r) * 2r) * v by Def4
.= (- (1r + 1r)) * v ; ::_thesis: verum
end;

theorem :: CLVECT_1:19
for V being ComplexLinearSpace
for v being VECTOR of V holds Sum <*v,v,v*> = ((1r + 1r) + 1r) * v
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V holds Sum <*v,v,v*> = ((1r + 1r) + 1r) * v
let v be VECTOR of V; ::_thesis: Sum <*v,v,v*> = ((1r + 1r) + 1r) * v
reconsider 2r = 2 + (0 * <i>) as Element of COMPLEX by XCMPLX_0:def_2;
thus  Sum <*v,v,v*> = (Sum <*v,v*>) + v by RLVECT_1:66
.= ((1r + 1r) * v) + v by Th17
.= ((1r + 1r) * v) + (1r * v) by Def5
.= ((1r + 1r) + 1r) * v by Def3 ; ::_thesis: verum
end;

begin


definition
let V be ComplexLinearSpace;
let V1 be Subset of V;
attrV1 is linearly-closed  means :Def7: :: CLVECT_1:def 7
( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for z being Complex
for v being VECTOR of V st v in V1 holds
z * v in V1 ) );
end;

:: deftheorem Def7 defines linearly-closed CLVECT_1:def_7_:_
 for V being ComplexLinearSpace
for V1 being Subset of V holds
( V1 is linearly-closed iff ( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for z being Complex
for v being VECTOR of V st v in V1 holds
z * v in V1 ) ) );

theorem Th20: :: CLVECT_1:20
for V being ComplexLinearSpace
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
0. V in V1
proof
let V be ComplexLinearSpace; ::_thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
0. V in V1
let V1 be Subset of V; ::_thesis: ( V1 <> {} & V1 is linearly-closed implies 0. V in V1 )
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed ; ::_thesis: 0. V in V1
set x = the Element of V1;
reconsider x = the Element of V1 as Element of V by A1, TARSKI:def_3;
 0c * x in V1 by A1, A2, Def7;
hence  0. V in V1 by Th1; ::_thesis: verum
end;

theorem Th21: :: CLVECT_1:21
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is linearly-closed holds
for v being VECTOR of V st v in V1 holds
- v in V1
proof
let V be ComplexLinearSpace; ::_thesis: for V1 being Subset of V st V1 is linearly-closed holds
for v being VECTOR of V st v in V1 holds
- v in V1
let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed implies for v being VECTOR of V st v in V1 holds
- v in V1 )
assume A1: V1 is linearly-closed ; ::_thesis: for v being VECTOR of V st v in V1 holds
- v in V1
let v be VECTOR of V; ::_thesis: ( v in V1 implies - v in V1 )
assume  v in V1 ; ::_thesis: - v in V1
then  (- 1r) * v in V1 by A1, Def7;
hence  - v in V1 by Th3; ::_thesis: verum
end;

theorem :: CLVECT_1:22
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is linearly-closed holds
for v, u being VECTOR of V st v in V1 & u in V1 holds
v - u in V1
proof
let V be ComplexLinearSpace; ::_thesis: for V1 being Subset of V st V1 is linearly-closed holds
for v, u being VECTOR of V st v in V1 & u in V1 holds
v - u in V1
let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed implies for v, u being VECTOR of V st v in V1 & u in V1 holds
v - u in V1 )
assume A1: V1 is linearly-closed ; ::_thesis: for v, u being VECTOR of V st v in V1 & u in V1 holds
v - u in V1
let v, u be VECTOR of V; ::_thesis: ( v in V1 & u in V1 implies v - u in V1 )
assume that
A2: v in V1 and
A3: u in V1 ; ::_thesis: v - u in V1
 - u in V1 by A1, A3, Th21;
hence  v - u in V1 by A1, A2, Def7; ::_thesis: verum
end;

theorem Th23: :: CLVECT_1:23
for V being ComplexLinearSpace holds {(0. V)} is linearly-closed
proof
let V be ComplexLinearSpace; ::_thesis: {(0. V)} is linearly-closed
thus  for v, u being VECTOR of V st v in {(0. V)} & u in {(0. V)} holds
v + u in {(0. V)} :: according to CLVECT_1:def_7 ::_thesis: for z being Complex
for v being VECTOR of V st v in {(0. V)} holds
z * v in {(0. V)}
proof
let v, u be VECTOR of V; ::_thesis: ( v in {(0. V)} & u in {(0. V)} implies v + u in {(0. V)} )
assume  ( v in {(0. V)} & u in {(0. V)} ) ; ::_thesis: v + u in {(0. V)}
then  ( v = 0. V & u = 0. V ) by TARSKI:def_1;
then  v + u = 0. V by RLVECT_1:4;
hence  v + u in {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;
let z be Complex; ::_thesis: for v being VECTOR of V st v in {(0. V)} holds
z * v in {(0. V)}
let v be VECTOR of V; ::_thesis: ( v in {(0. V)} implies z * v in {(0. V)} )
assume A1: v in {(0. V)} ; ::_thesis: z * v in {(0. V)}
then  v = 0. V by TARSKI:def_1;
hence  z * v in {(0. V)} by A1, Th1; ::_thesis: verum
end;

theorem :: CLVECT_1:24
for V being ComplexLinearSpace
for V1 being Subset of V st the carrier of V = V1 holds
V1 is linearly-closed
proof
let V be ComplexLinearSpace; ::_thesis: for V1 being Subset of V st the carrier of V = V1 holds
V1 is linearly-closed
let V1 be Subset of V; ::_thesis: ( the carrier of V = V1 implies V1 is linearly-closed )
assume A1: the carrier of V = V1 ; ::_thesis: V1 is linearly-closed
hence  for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ; :: according to CLVECT_1:def_7 ::_thesis: for z being Complex
for v being VECTOR of V st v in V1 holds
z * v in V1
let z be Complex; ::_thesis: for v being VECTOR of V st v in V1 holds
z * v in V1
let v be VECTOR of V; ::_thesis: ( v in V1 implies z * v in V1 )
thus  ( v in V1 implies z * v in V1 ) by A1; ::_thesis: verum
end;

theorem :: CLVECT_1:25
for V being ComplexLinearSpace
for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 =  {  (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 )  }  holds
V3 is linearly-closed
proof
let V be ComplexLinearSpace; ::_thesis: for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 =  {  (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 )  }  holds
V3 is linearly-closed
let V1, V2, V3 be Subset of V; ::_thesis: ( V1 is linearly-closed & V2 is linearly-closed & V3 =  {  (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 )  }  implies V3 is linearly-closed )
assume that
A1: ( V1 is linearly-closed & V2 is linearly-closed ) and
A2: V3 =  {  (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 )  }  ; ::_thesis: V3 is linearly-closed
thus  for v, u being VECTOR of V st v in V3 & u in V3 holds
v + u in V3 :: according to CLVECT_1:def_7 ::_thesis: for z being Complex
for v being VECTOR of V st v in V3 holds
z * v in V3
proof
let v, u be VECTOR of V; ::_thesis: ( v in V3 & u in V3 implies v + u in V3 )
assume that
A3: v in V3 and
A4: u in V3 ; ::_thesis: v + u in V3
consider v1, v2 being VECTOR of V such that
A5: v = v1 + v2 and
A6: ( v1 in V1 & v2 in V2 ) by A2, A3;
consider u1, u2 being VECTOR of V such that
A7: u = u1 + u2 and
A8: ( u1 in V1 & u2 in V2 ) by A2, A4;
A9: v + u = ((v1 + v2) + u1) + u2 by A5, A7, RLVECT_1:def_3
.= ((v1 + u1) + v2) + u2 by RLVECT_1:def_3
.= (v1 + u1) + (v2 + u2) by RLVECT_1:def_3 ;
 ( v1 + u1 in V1 & v2 + u2 in V2 ) by A1, A6, A8, Def7;
hence  v + u in V3 by A2, A9; ::_thesis: verum
end;
let z be Complex; ::_thesis: for v being VECTOR of V st v in V3 holds
z * v in V3
let v be VECTOR of V; ::_thesis: ( v in V3 implies z * v in V3 )
assume  v in V3 ; ::_thesis: z * v in V3
then consider v1, v2 being VECTOR of V such that
A10: v = v1 + v2 and
A11: ( v1 in V1 & v2 in V2 ) by A2;
A12: z * v = (z * v1) + (z * v2) by A10, Def2;
 ( z * v1 in V1 & z * v2 in V2 ) by A1, A11, Def7;
hence  z * v in V3 by A2, A12; ::_thesis: verum
end;

theorem :: CLVECT_1:26
for V being ComplexLinearSpace
for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds
V1 /\ V2 is linearly-closed
proof
let V be ComplexLinearSpace; ::_thesis: for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds
V1 /\ V2 is linearly-closed
let V1, V2 be Subset of V; ::_thesis: ( V1 is linearly-closed & V2 is linearly-closed implies V1 /\ V2 is linearly-closed )
assume that
A1: V1 is linearly-closed and
A2: V2 is linearly-closed ; ::_thesis: V1 /\ V2 is linearly-closed
thus  for v, u being VECTOR of V st v in V1 /\ V2 & u in V1 /\ V2 holds
v + u in V1 /\ V2 :: according to CLVECT_1:def_7 ::_thesis: for z being Complex
for v being VECTOR of V st v in V1 /\ V2 holds
z * v in V1 /\ V2
proof
let v, u be VECTOR of V; ::_thesis: ( v in V1 /\ V2 & u in V1 /\ V2 implies v + u in V1 /\ V2 )
assume A3: ( v in V1 /\ V2 & u in V1 /\ V2 ) ; ::_thesis: v + u in V1 /\ V2
then  ( v in V2 & u in V2 ) by XBOOLE_0:def_4;
then A4: v + u in V2 by A2, Def7;
 ( v in V1 & u in V1 ) by A3, XBOOLE_0:def_4;
then  v + u in V1 by A1, Def7;
hence  v + u in V1 /\ V2 by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
let z be Complex; ::_thesis: for v being VECTOR of V st v in V1 /\ V2 holds
z * v in V1 /\ V2
let v be VECTOR of V; ::_thesis: ( v in V1 /\ V2 implies z * v in V1 /\ V2 )
assume A5: v in V1 /\ V2 ; ::_thesis: z * v in V1 /\ V2
then  v in V2 by XBOOLE_0:def_4;
then A6: z * v in V2 by A2, Def7;
 v in V1 by A5, XBOOLE_0:def_4;
then  z * v in V1 by A1, Def7;
hence  z * v in V1 /\ V2 by A6, XBOOLE_0:def_4; ::_thesis: verum
end;

definition
let V be ComplexLinearSpace;
mode Subspace of V ->  ComplexLinearSpace means :Def8: :: CLVECT_1:def 8
( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V || the carrier of it & the Mult of it = the Mult of V | [:COMPLEX, the carrier of it:] );
existence
 ex b1 being ComplexLinearSpace st
( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:COMPLEX, the carrier of b1:] )
proof
 ( the addF of V = the addF of V || the carrier of V & the Mult of V = the Mult of V | [:COMPLEX, the carrier of V:] ) by RELSET_1:19;
hence  ex b1 being ComplexLinearSpace st
( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:COMPLEX, the carrier of b1:] ) ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Subspace CLVECT_1:def_8_:_
 for V, b2 being ComplexLinearSpace holds
( b2 is Subspace of V iff ( the carrier of b2 c= the carrier of V & 0. b2 = 0. V & the addF of b2 = the addF of V || the carrier of b2 & the Mult of b2 = the Mult of V | [:COMPLEX, the carrier of b2:] ) );


theorem :: CLVECT_1:27
for V being ComplexLinearSpace
for W1, W2 being Subspace of V
for x being set st x in W1 & W1 is Subspace of W2 holds
x in W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being Subspace of V
for x being set st x in W1 & W1 is Subspace of W2 holds
x in W2
let W1, W2 be Subspace of V; ::_thesis: for x being set st x in W1 & W1 is Subspace of W2 holds
x in W2
let x be set ; ::_thesis: ( x in W1 & W1 is Subspace of W2 implies x in W2 )
assume  ( x in W1 & W1 is Subspace of W2 ) ; ::_thesis: x in W2
then  ( x in the carrier of W1 & the carrier of W1 c= the carrier of W2 ) by Def8, STRUCT_0:def_5;
hence  x in W2 by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th28: :: CLVECT_1:28
for V being ComplexLinearSpace
for W being Subspace of V
for x being set st x in W holds
x in V
proof
let V be ComplexLinearSpace; ::_thesis: for W being Subspace of V
for x being set st x in W holds
x in V
let W be Subspace of V; ::_thesis: for x being set st x in W holds
x in V
let x be set ; ::_thesis: ( x in W implies x in V )
assume  x in W ; ::_thesis: x in V
then A1: x in the carrier of W by STRUCT_0:def_5;
 the carrier of W c= the carrier of V by Def8;
hence  x in V by A1, STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th29: :: CLVECT_1:29
for V being ComplexLinearSpace
for W being Subspace of V
for w being VECTOR of W holds w is VECTOR of V
proof
let V be ComplexLinearSpace; ::_thesis: for W being Subspace of V
for w being VECTOR of W holds w is VECTOR of V
let W be Subspace of V; ::_thesis: for w being VECTOR of W holds w is VECTOR of V
let w be VECTOR of W; ::_thesis: w is VECTOR of V
 w in V by Th28, RLVECT_1:1;
hence  w is VECTOR of V by STRUCT_0:def_5; ::_thesis: verum
end;

theorem :: CLVECT_1:30
for V being ComplexLinearSpace
for W being Subspace of V holds 0. W = 0. V by Def8;

theorem :: CLVECT_1:31
for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds 0. W1 = 0. W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds 0. W1 = 0. W2
let W1, W2 be Subspace of V; ::_thesis: 0. W1 = 0. W2
thus  0. W1 = 0. V by Def8
.= 0. W2 by Def8 ; ::_thesis: verum
end;

theorem Th32: :: CLVECT_1:32
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
let v, u be VECTOR of V; ::_thesis: for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
let W be Subspace of V; ::_thesis: for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u
let w1, w2 be VECTOR of W; ::_thesis: ( w1 = v & w2 = u implies w1 + w2 = v + u )
assume A1: ( v = w1 & u = w2 ) ; ::_thesis: w1 + w2 = v + u
 w1 + w2 = ( the addF of V || the carrier of W) . [w1,w2] by Def8;
hence  w1 + w2 = v + u by A1, FUNCT_1:49; ::_thesis: verum
end;

theorem Th33: :: CLVECT_1:33
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V
for w being VECTOR of W st w = v holds
z * w = z * v
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V
for w being VECTOR of W st w = v holds
z * w = z * v
let v be VECTOR of V; ::_thesis: for z being Complex
for W being Subspace of V
for w being VECTOR of W st w = v holds
z * w = z * v
let z be Complex; ::_thesis: for W being Subspace of V
for w being VECTOR of W st w = v holds
z * w = z * v
let W be Subspace of V; ::_thesis: for w being VECTOR of W st w = v holds
z * w = z * v
let w be VECTOR of W; ::_thesis: ( w = v implies z * w = z * v )
reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2;
 z * w = ( the Mult of V | [:COMPLEX, the carrier of W:]) . [z,w] by Def8;
hence  ( w = v implies z * w = z * v ) by FUNCT_1:49; ::_thesis: verum
end;

theorem Th34: :: CLVECT_1:34
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V
for w being VECTOR of W st w = v holds
- v = - w
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W being Subspace of V
for w being VECTOR of W st w = v holds
- v = - w
let v be VECTOR of V; ::_thesis: for W being Subspace of V
for w being VECTOR of W st w = v holds
- v = - w
let W be Subspace of V; ::_thesis: for w being VECTOR of W st w = v holds
- v = - w
let w be VECTOR of W; ::_thesis: ( w = v implies - v = - w )
assume A1: w = v ; ::_thesis: - v = - w
 ( - v = (- 1r) * v & - w = (- 1r) * w ) by Th3;
hence  - v = - w by A1, Th33; ::_thesis: verum
end;

theorem Th35: :: CLVECT_1:35
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
let v, u be VECTOR of V; ::_thesis: for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
let W be Subspace of V; ::_thesis: for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u
let w1, w2 be VECTOR of W; ::_thesis: ( w1 = v & w2 = u implies w1 - w2 = v - u )
assume that
A1: w1 = v and
A2: w2 = u ; ::_thesis: w1 - w2 = v - u
 - w2 = - u by A2, Th34;
hence  w1 - w2 = v - u by A1, Th32; ::_thesis: verum
end;

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
proof
let V be ComplexLinearSpace; ::_thesis: for V1 being Subset of V
for W being Subspace of V st the carrier of W = V1 holds
V1 is linearly-closed
let V1 be Subset of V; ::_thesis: for W being Subspace of V st the carrier of W = V1 holds
V1 is linearly-closed
let W be Subspace of V; ::_thesis: ( the carrier of W = V1 implies V1 is linearly-closed )
set VW = the carrier of W;
reconsider WW = W as ComplexLinearSpace ;
assume A1: the carrier of W = V1 ; ::_thesis: V1 is linearly-closed
thus  for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 :: according to CLVECT_1:def_7 ::_thesis: for z being Complex
for v being VECTOR of V st v in V1 holds
z * v in V1
proof
let v, u be VECTOR of V; ::_thesis: ( v in V1 & u in V1 implies v + u in V1 )
assume  ( v in V1 & u in V1 ) ; ::_thesis: v + u in V1
then reconsider vv = v, uu = u as VECTOR of WW by A1;
reconsider vw = vv + uu as Element of the carrier of W ;
 vw in V1 by A1;
hence  v + u in V1 by Th32; ::_thesis: verum
end;
let z be Complex; ::_thesis: for v being VECTOR of V st v in V1 holds
z * v in V1
let v be VECTOR of V; ::_thesis: ( v in V1 implies z * v in V1 )
assume  v in V1 ; ::_thesis: z * v in V1
then reconsider vv = v as VECTOR of WW by A1;
reconsider vw = z * vv as Element of the carrier of W ;
 vw in V1 by A1;
hence  z * v in V1 by Th33; ::_thesis: verum
end;

theorem Th36: :: CLVECT_1:36
for V being ComplexLinearSpace
for W being Subspace of V holds 0. V in W
proof
let V be ComplexLinearSpace; ::_thesis: for W being Subspace of V holds 0. V in W
let W be Subspace of V; ::_thesis: 0. V in W
 0. W in W by RLVECT_1:1;
hence  0. V in W by Def8; ::_thesis: verum
end;

theorem :: CLVECT_1:37
for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds 0. W1 in W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds 0. W1 in W2
let W1, W2 be Subspace of V; ::_thesis: 0. W1 in W2
 0. W1 = 0. V by Def8;
hence  0. W1 in W2 by Th36; ::_thesis: verum
end;

theorem :: CLVECT_1:38
for V being ComplexLinearSpace
for W being Subspace of V holds 0. W in V by Th28, RLVECT_1:1;

theorem Th39: :: CLVECT_1:39
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in W & v in W holds
u + v in W
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V st u in W & v in W holds
u + v in W
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V st u in W & v in W holds
u + v in W
let W be Subspace of V; ::_thesis: ( u in W & v in W implies u + v in W )
reconsider VW = the carrier of W as Subset of V by Def8;
assume  ( u in W & v in W ) ; ::_thesis: u + v in W
then A1: ( u in the carrier of W & v in the carrier of W ) by STRUCT_0:def_5;
 VW is linearly-closed by Lm3;
then  u + v in the carrier of W by A1, Def7;
hence  u + v in W by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th40: :: CLVECT_1:40
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
z * v in W
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
z * v in W
let v be VECTOR of V; ::_thesis: for z being Complex
for W being Subspace of V st v in W holds
z * v in W
let z be Complex; ::_thesis: for W being Subspace of V st v in W holds
z * v in W
let W be Subspace of V; ::_thesis: ( v in W implies z * v in W )
reconsider VW = the carrier of W as Subset of V by Def8;
assume  v in W ; ::_thesis: z * v in W
then A1: v in the carrier of W by STRUCT_0:def_5;
 VW is linearly-closed by Lm3;
then  z * v in the carrier of W by A1, Def7;
hence  z * v in W by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th41: :: CLVECT_1:41
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V st v in W holds
- v in W
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W being Subspace of V st v in W holds
- v in W
let v be VECTOR of V; ::_thesis: for W being Subspace of V st v in W holds
- v in W
let W be Subspace of V; ::_thesis: ( v in W implies - v in W )
assume  v in W ; ::_thesis: - v in W
then  (- 1r) * v in W by Th40;
hence  - v in W by Th3; ::_thesis: verum
end;

theorem Th42: :: CLVECT_1:42
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in W & v in W holds
u - v in W
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V st u in W & v in W holds
u - v in W
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V st u in W & v in W holds
u - v in W
let W be Subspace of V; ::_thesis: ( u in W & v in W implies u - v in W )
assume A1: u in W ; ::_thesis: ( not v in W or u - v in W )
assume  v in W ; ::_thesis: u - v in W
then  - v in W by Th41;
hence  u - v in W by A1, Th39; ::_thesis: verum
end;


Lm4: now__::_thesis:_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; ::_thesis: 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 V1 be Subset of V; ::_thesis: 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 D be non empty set ; ::_thesis: 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 d1 be Element of D; ::_thesis: 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 A be BinOp of D; ::_thesis: 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 M be Function of [:COMPLEX,D:],D; ::_thesis: 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 z be Complex; ::_thesis: 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 w be VECTOR of CLSStruct(# D,d1,A,M #); ::_thesis: 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 Element of V; ::_thesis: ( 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 ; ::_thesis: 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; ::_thesis: verum
end;

theorem Th43: :: CLVECT_1:43
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 st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
proof
let V be ComplexLinearSpace; ::_thesis: 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 st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let V1 be Subset of V; ::_thesis: 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 st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let D be non empty set ; ::_thesis: for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let d1 be Element of D; ::_thesis: for A being BinOp of D
for M being Function of [:COMPLEX,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let A be BinOp of D; ::_thesis: for M being Function of [:COMPLEX,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let M be Function of [:COMPLEX,D:],D; ::_thesis: ( V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] implies CLSStruct(# D,d1,A,M #) is Subspace of V )
assume that
A1: V1 = D and
A2: d1 = 0. V and
A3: A = the addF of V || V1 and
A4: M = the Mult of V | [:COMPLEX,V1:] ; ::_thesis: CLSStruct(# D,d1,A,M #) is Subspace of V
set W = CLSStruct(# D,d1,A,M #);
A5: for x, y being VECTOR of CLSStruct(# D,d1,A,M #) holds x + y = the addF of V . [x,y] by A1, A3, FUNCT_1:49;
A6: ( CLSStruct(# D,d1,A,M #) is Abelian & CLSStruct(# D,d1,A,M #) is add-associative & CLSStruct(# D,d1,A,M #) is right_zeroed & CLSStruct(# D,d1,A,M #) is right_complementable & CLSStruct(# D,d1,A,M #) is vector-distributive & CLSStruct(# D,d1,A,M #) is scalar-distributive & CLSStruct(# D,d1,A,M #) is scalar-associative & CLSStruct(# D,d1,A,M #) is scalar-unital )
proof
set MV = the Mult of V;
set AV = the addF of V;
thus  for x, y being VECTOR of CLSStruct(# D,d1,A,M #) holds x + y = y + x :: according to RLVECT_1:def_2 ::_thesis: ( CLSStruct(# D,d1,A,M #) is add-associative & CLSStruct(# D,d1,A,M #) is right_zeroed & CLSStruct(# D,d1,A,M #) is right_complementable & CLSStruct(# D,d1,A,M #) is vector-distributive & CLSStruct(# D,d1,A,M #) is scalar-distributive & CLSStruct(# D,d1,A,M #) is scalar-associative & CLSStruct(# D,d1,A,M #) is scalar-unital )
proof
let x, y be VECTOR of CLSStruct(# D,d1,A,M #); ::_thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def_3;
thus x + y = x1 + y1 by A5
.= y1 + x1
.= y + x by A5 ; ::_thesis: verum
end;
thus  for x, y, z being VECTOR of CLSStruct(# D,d1,A,M #) holds (x + y) + z = x + (y + z) :: according to RLVECT_1:def_3 ::_thesis: ( CLSStruct(# D,d1,A,M #) is right_zeroed & CLSStruct(# D,d1,A,M #) is right_complementable & CLSStruct(# D,d1,A,M #) is vector-distributive & CLSStruct(# D,d1,A,M #) is scalar-distributive & CLSStruct(# D,d1,A,M #) is scalar-associative & CLSStruct(# D,d1,A,M #) is scalar-unital )
proof
let x, y, z be VECTOR of CLSStruct(# D,d1,A,M #); ::_thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def_3;
thus (x + y) + z = the addF of V . [(x + y),z1] by A5
.= (x1 + y1) + z1 by A5
.= x1 + (y1 + z1) by RLVECT_1:def_3
.= the addF of V . [x1,(y + z)] by A5
.= x + (y + z) by A5 ; ::_thesis: verum
end;
thus  for x being VECTOR of CLSStruct(# D,d1,A,M #) holds x + (0. CLSStruct(# D,d1,A,M #)) = x :: according to RLVECT_1:def_4 ::_thesis: ( CLSStruct(# D,d1,A,M #) is right_complementable & CLSStruct(# D,d1,A,M #) is vector-distributive & CLSStruct(# D,d1,A,M #) is scalar-distributive & CLSStruct(# D,d1,A,M #) is scalar-associative & CLSStruct(# D,d1,A,M #) is scalar-unital )
proof
let x be VECTOR of CLSStruct(# D,d1,A,M #); ::_thesis: x + (0. CLSStruct(# D,d1,A,M #)) = x
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
thus x + (0. CLSStruct(# D,d1,A,M #)) = y + (0. V) by A2, A5
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
thus  CLSStruct(# D,d1,A,M #) is right_complementable ::_thesis: ( CLSStruct(# D,d1,A,M #) is vector-distributive & CLSStruct(# D,d1,A,M #) is scalar-distributive & CLSStruct(# D,d1,A,M #) is scalar-associative & CLSStruct(# D,d1,A,M #) is scalar-unital )
proof
let x be VECTOR of CLSStruct(# D,d1,A,M #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x1 = x as VECTOR of V by A1, TARSKI:def_3;
consider v being VECTOR of V such that
A7: x1 + v = 0. V by ALGSTR_0:def_11;
v = - x1 by A7, RLVECT_1:def_10
.= (- 1r) * x1 by Th3
.= the Mult of V . [(- 1r),x]
.= (- 1r) * x by A1, A4, FUNCT_1:49 ;
then reconsider y = v as VECTOR of CLSStruct(# D,d1,A,M #) ;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. CLSStruct(# D,d1,A,M #)
thus  x + y = 0. CLSStruct(# D,d1,A,M #) by A2, A5, A7; ::_thesis: verum
end;
thus  for z being Complex
for x, y being VECTOR of CLSStruct(# D,d1,A,M #) holds z * (x + y) = (z * x) + (z * y) :: according to CLVECT_1:def_2 ::_thesis: ( CLSStruct(# D,d1,A,M #) is scalar-distributive & CLSStruct(# D,d1,A,M #) is scalar-associative & CLSStruct(# D,d1,A,M #) is scalar-unital )
proof
let z be Complex; ::_thesis: for x, y being VECTOR of CLSStruct(# D,d1,A,M #) holds z * (x + y) = (z * x) + (z * y)
let x, y be VECTOR of CLSStruct(# D,d1,A,M #); ::_thesis: z * (x + y) = (z * x) + (z * y)
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def_3;
A8: ( z * x1 = z * x & z * y1 = z * y ) by A1, A4, Lm4;
thus z * (x + y) = z * (x1 + y1) by A1, A4, A5, Lm4
.= (z * x1) + (z * y1) by Def2
.= (z * x) + (z * y) by A5, A8 ; ::_thesis: verum
end;
thus  for z1, z2 being Complex
for x being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) :: according to CLVECT_1:def_3 ::_thesis: ( CLSStruct(# D,d1,A,M #) is scalar-associative & CLSStruct(# D,d1,A,M #) is scalar-unital )
proof
let z1, z2 be Complex; ::_thesis: for x being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 + z2) * x = (z1 * x) + (z2 * x)
let x be VECTOR of CLSStruct(# D,d1,A,M #); ::_thesis: (z1 + z2) * x = (z1 * x) + (z2 * x)
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
A9: ( z1 * y = z1 * x & z2 * y = z2 * x ) by A1, A4, Lm4;
thus (z1 + z2) * x = (z1 + z2) * y by A1, A4, Lm4
.= (z1 * y) + (z2 * y) by Def3
.= (z1 * x) + (z2 * x) by A5, A9 ; ::_thesis: verum
end;
thus  for z1, z2 being Complex
for x being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 * z2) * x = z1 * (z2 * x) :: according to CLVECT_1:def_4 ::_thesis: CLSStruct(# D,d1,A,M #) is scalar-unital
proof
let z1, z2 be Complex; ::_thesis: for x being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 * z2) * x = z1 * (z2 * x)
let x be VECTOR of CLSStruct(# D,d1,A,M #); ::_thesis: (z1 * z2) * x = z1 * (z2 * x)
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
A10: z2 * y = z2 * x by A1, A4, Lm4;
thus (z1 * z2) * x = (z1 * z2) * y by A1, A4, Lm4
.= z1 * (z2 * y) by Def4
.= z1 * (z2 * x) by A1, A4, A10, Lm4 ; ::_thesis: verum
end;
let x be VECTOR of CLSStruct(# D,d1,A,M #); :: according to CLVECT_1:def_5 ::_thesis: 1r * x = x
reconsider y = x as VECTOR of V by A1, TARSKI:def_3;
thus 1r * x = 1r * y by A1, A4, Lm4
.= x by Def5 ; ::_thesis: verum
end;
 0. CLSStruct(# D,d1,A,M #) = 0. V by A2;
hence  CLSStruct(# D,d1,A,M #) is Subspace of V by A1, A3, A4, A6, Def8; ::_thesis: verum
end;

theorem Th44: :: CLVECT_1:44
for V being ComplexLinearSpace holds V is Subspace of V
proof
let V be ComplexLinearSpace; ::_thesis: V is Subspace of V
thus  ( the carrier of V c= the carrier of V & 0. V = 0. V ) ; :: according to CLVECT_1:def_8 ::_thesis: ( the addF of V = the addF of V || the carrier of V & the Mult of V = the Mult of V | [:COMPLEX, the carrier of V:] )
thus  ( the addF of V = the addF of V || the carrier of V & the Mult of V = the Mult of V | [:COMPLEX, the carrier of V:] ) by RELSET_1:19; ::_thesis: verum
end;

theorem Th45: :: CLVECT_1:45
for V, X being strict ComplexLinearSpace st V is Subspace of X & X is Subspace of V holds
V = X
proof
let V, X be strict ComplexLinearSpace; ::_thesis: ( V is Subspace of X & X is Subspace of V implies V = X )
assume that
A1: V is Subspace of X and
A2: X is Subspace of V ; ::_thesis: V = X
set VX = the carrier of X;
set VV = the carrier of V;
 ( the carrier of V c= the carrier of X & the carrier of X c= the carrier of V ) by A1, A2, Def8;
then A3: the carrier of V = the carrier of X by XBOOLE_0:def_10;
set AX = the addF of X;
set AV = the addF of V;
 ( the addF of V = the addF of X || the carrier of V & the addF of X = the addF of V || the carrier of X ) by A1, A2, Def8;
then A4: the addF of V = the addF of X by A3, RELAT_1:72;
set MX = the Mult of X;
set MV = the Mult of V;
A5: the Mult of X = the Mult of V | [:COMPLEX, the carrier of X:] by A2, Def8;
 ( 0. V = 0. X & the Mult of V = the Mult of X | [:COMPLEX, the carrier of V:] ) by A1, Def8;
hence  V = X by A3, A4, A5, RELAT_1:72; ::_thesis: verum
end;

theorem Th46: :: CLVECT_1:46
for V, X, Y being ComplexLinearSpace st V is Subspace of X & X is Subspace of Y holds
V is Subspace of Y
proof
let V, X, Y be ComplexLinearSpace; ::_thesis: ( V is Subspace of X & X is Subspace of Y implies V is Subspace of Y )
assume that
A1: V is Subspace of X and
A2: X is Subspace of Y ; ::_thesis: V is Subspace of Y
 ( the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y ) by A1, A2, Def8;
hence  the carrier of V c= the carrier of Y by XBOOLE_1:1; :: according to CLVECT_1:def_8 ::_thesis: ( 0. V = 0. Y & the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:COMPLEX, the carrier of V:] )
 0. V = 0. X by A1, Def8;
hence  0. V = 0. Y by A2, Def8; ::_thesis: ( the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:COMPLEX, the carrier of V:] )
thus  the addF of V = the addF of Y || the carrier of V ::_thesis: the Mult of V = the Mult of Y | [:COMPLEX, the carrier of V:]
proof
set AY = the addF of Y;
set VX = the carrier of X;
set AX = the addF of X;
set VV = the carrier of V;
set AV = the addF of V;
 the carrier of V c= the carrier of X by A1, Def8;
then A3: [: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:] by ZFMISC_1:96;
 the addF of V = the addF of X || the carrier of V by A1, Def8;
then  the addF of V = ( the addF of Y || the carrier of X) || the carrier of V by A2, Def8;
hence  the addF of V = the addF of Y || the carrier of V by A3, FUNCT_1:51; ::_thesis: verum
end;
set MY = the Mult of Y;
set MX = the Mult of X;
set MV = the Mult of V;
set VX = the carrier of X;
set VV = the carrier of V;
 the carrier of V c= the carrier of X by A1, Def8;
then A4: [:COMPLEX, the carrier of V:] c= [:COMPLEX, the carrier of X:] by ZFMISC_1:95;
 the Mult of V = the Mult of X | [:COMPLEX, the carrier of V:] by A1, Def8;
then  the Mult of V = ( the Mult of Y | [:COMPLEX, the carrier of X:]) | [:COMPLEX, the carrier of V:] by A2, Def8;
hence  the Mult of V = the Mult of Y | [:COMPLEX, the carrier of V:] by A4, FUNCT_1:51; ::_thesis: verum
end;

theorem Th47: :: CLVECT_1:47
for V being ComplexLinearSpace
for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 is Subspace of W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 is Subspace of W2
let W1, W2 be Subspace of V; ::_thesis: ( the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2 )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
set AV = the addF of V;
set MV = the Mult of V;
assume A1: the carrier of W1 c= the carrier of W2 ; ::_thesis: W1 is Subspace of W2
then A2: [: the carrier of W1, the carrier of W1:] c= [: the carrier of W2, the carrier of W2:] by ZFMISC_1:96;
 0. W1 = 0. V by Def8;
hence  ( the carrier of W1 c= the carrier of W2 & 0. W1 = 0. W2 ) by A1, Def8; :: according to CLVECT_1:def_8 ::_thesis: ( the addF of W1 = the addF of W2 || the carrier of W1 & the Mult of W1 = the Mult of W2 | [:COMPLEX, the carrier of W1:] )
 ( the addF of W1 = the addF of V || the carrier of W1 & the addF of W2 = the addF of V || the carrier of W2 ) by Def8;
hence  the addF of W1 = the addF of W2 || the carrier of W1 by A2, FUNCT_1:51; ::_thesis: the Mult of W1 = the Mult of W2 | [:COMPLEX, the carrier of W1:]
A3: [:COMPLEX, the carrier of W1:] c= [:COMPLEX, the carrier of W2:] by A1, ZFMISC_1:95;
 ( the Mult of W1 = the Mult of V | [:COMPLEX, the carrier of W1:] & the Mult of W2 = the Mult of V | [:COMPLEX, the carrier of W2:] ) by Def8;
hence  the Mult of W1 = the Mult of W2 | [:COMPLEX, the carrier of W1:] by A3, FUNCT_1:51; ::_thesis: verum
end;

theorem :: CLVECT_1:48
for V being ComplexLinearSpace
for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds
v in W2 ) holds
W1 is Subspace of W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds
v in W2 ) holds
W1 is Subspace of W2
let W1, W2 be Subspace of V; ::_thesis: ( ( for v being VECTOR of V st v in W1 holds
v in W2 ) implies W1 is Subspace of W2 )
assume A1: for v being VECTOR of V st v in W1 holds
v in W2 ; ::_thesis: W1 is Subspace of W2
 the carrier of W1 c= the carrier of W2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of W2 )
assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of W2
 the carrier of W1 c= the carrier of V by Def8;
then reconsider v = x as VECTOR of V by A2;
 v in W1 by A2, STRUCT_0:def_5;
then  v in W2 by A1;
hence  x in the carrier of W2 by STRUCT_0:def_5; ::_thesis: verum
end;
hence  W1 is Subspace of W2 by Th47; ::_thesis: verum
end;

registration
let V be ComplexLinearSpace;
cluster non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for Subspace of V;
existence
 ex b1 being Subspace of V st b1 is strict
proof
 ( the carrier of V is Subset of V iff the carrier of V c= the carrier of V ) ;
then reconsider V1 = the carrier of V as Subset of V ;
 ( the addF of V = the addF of V || V1 & the Mult of V = the Mult of V | [:COMPLEX,V1:] ) by RELSET_1:19;
then  CLSStruct(# the carrier of V,(0. V), the addF of V, the Mult of V #) is Subspace of V by Th43;
hence  ex b1 being Subspace of V st b1 is strict ; ::_thesis: verum
end;
end;

theorem Th49: :: CLVECT_1:49
for V being ComplexLinearSpace
for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds
W1 = W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds
W1 = W2
let W1, W2 be strict Subspace of V; ::_thesis: ( the carrier of W1 = the carrier of W2 implies W1 = W2 )
assume  the carrier of W1 = the carrier of W2 ; ::_thesis: W1 = W2
then  ( W1 is Subspace of W2 & W2 is Subspace of W1 ) by Th47;
hence  W1 = W2 by Th45; ::_thesis: verum
end;

theorem Th50: :: CLVECT_1:50
for V being ComplexLinearSpace
for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2
let W1, W2 be strict Subspace of V; ::_thesis: ( ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) implies W1 = W2 )
assume A1: for v being VECTOR of V holds
( v in W1 iff v in W2 ) ; ::_thesis: W1 = W2
 for x being set holds
( x in the carrier of W1 iff x in the carrier of W2 )
proof
let x be set ; ::_thesis: ( x in the carrier of W1 iff x in the carrier of W2 )
thus  ( x in the carrier of W1 implies x in the carrier of W2 ) ::_thesis: ( x in the carrier of W2 implies x in the carrier of W1 )
proof
assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of W2
 the carrier of W1 c= the carrier of V by Def8;
then reconsider v = x as VECTOR of V by A2;
 v in W1 by A2, STRUCT_0:def_5;
then  v in W2 by A1;
hence  x in the carrier of W2 by STRUCT_0:def_5; ::_thesis: verum
end;
assume A3: x in the carrier of W2 ; ::_thesis: x in the carrier of W1
 the carrier of W2 c= the carrier of V by Def8;
then reconsider v = x as VECTOR of V by A3;
 v in W2 by A3, STRUCT_0:def_5;
then  v in W1 by A1;
hence  x in the carrier of W1 by STRUCT_0:def_5; ::_thesis: verum
end;
then  the carrier of W1 = the carrier of W2 by TARSKI:1;
hence  W1 = W2 by Th49; ::_thesis: verum
end;

theorem :: CLVECT_1:51
for V being strict ComplexLinearSpace
for W being strict Subspace of V st the carrier of W = the carrier of V holds
W = V
proof
let V be strict ComplexLinearSpace; ::_thesis: for W being strict Subspace of V st the carrier of W = the carrier of V holds
W = V
let W be strict Subspace of V; ::_thesis: ( the carrier of W = the carrier of V implies W = V )
assume A1: the carrier of W = the carrier of V ; ::_thesis: W = V
 V is Subspace of V by Th44;
hence  W = V by A1, Th49; ::_thesis: verum
end;

theorem :: CLVECT_1:52
for V being strict ComplexLinearSpace
for W being strict Subspace of V st ( for v being VECTOR of V holds
( v in W iff v in V ) ) holds
W = V
proof
let V be strict ComplexLinearSpace; ::_thesis: for W being strict Subspace of V st ( for v being VECTOR of V holds
( v in W iff v in V ) ) holds
W = V
let W be strict Subspace of V; ::_thesis: ( ( for v being VECTOR of V holds
( v in W iff v in V ) ) implies W = V )
assume A1: for v being VECTOR of V holds
( v in W iff v in V ) ; ::_thesis: W = V
 V is Subspace of V by Th44;
hence  W = V by A1, Th50; ::_thesis: verum
end;

theorem :: CLVECT_1:53
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 by Lm3;

theorem Th54: :: CLVECT_1:54
for V being ComplexLinearSpace
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
proof
let V be ComplexLinearSpace; ::_thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W
let V1 be Subset of V; ::_thesis: ( V1 <> {} & V1 is linearly-closed implies ex W being strict Subspace of V st V1 = the carrier of W )
assume that
A1: V1 <> {} and
A2: V1 is linearly-closed ; ::_thesis: ex W being strict Subspace of V st V1 = the carrier of W
reconsider D = V1 as non empty set by A1;
set M = the Mult of V | [:COMPLEX,V1:];
set VV = the carrier of V;
 dom the Mult of V = [:COMPLEX, the carrier of V:] by FUNCT_2:def_1;
then A3: dom ( the Mult of V | [:COMPLEX,V1:]) = [:COMPLEX, the carrier of V:] /\ [:COMPLEX,V1:] by RELAT_1:61;
 [:COMPLEX,V1:] c= [:COMPLEX, the carrier of V:] by ZFMISC_1:95;
then A4: dom ( the Mult of V | [:COMPLEX,V1:]) = [:COMPLEX,D:] by A3, XBOOLE_1:28;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_D_implies_ex_x_being_set_st_
(_x_in_dom_(_the_Mult_of_V_|_[:COMPLEX,V1:])_&_y_=_(_the_Mult_of_V_|_[:COMPLEX,V1:])_._x_)_)_&_(_ex_x_being_set_st_
(_x_in_dom_(_the_Mult_of_V_|_[:COMPLEX,V1:])_&_y_=_(_the_Mult_of_V_|_[:COMPLEX,V1:])_._x_)_implies_y_in_D_)_)
let y be set ; ::_thesis: ( ( y in D implies ex x being set st
( x in dom ( the Mult of V | [:COMPLEX,V1:]) & y = ( the Mult of V | [:COMPLEX,V1:]) . x ) ) & ( ex x being set st
( x in dom ( the Mult of V | [:COMPLEX,V1:]) & y = ( the Mult of V | [:COMPLEX,V1:]) . x ) implies y in D ) )
thus  ( y in D implies ex x being set st
( x in dom ( the Mult of V | [:COMPLEX,V1:]) & y = ( the Mult of V | [:COMPLEX,V1:]) . x ) ) ::_thesis: ( ex x being set st
( x in dom ( the Mult of V | [:COMPLEX,V1:]) & y = ( the Mult of V | [:COMPLEX,V1:]) . x ) implies y in D )
proof
assume A5: y in D ; ::_thesis: ex x being set st
( x in dom ( the Mult of V | [:COMPLEX,V1:]) & y = ( the Mult of V | [:COMPLEX,V1:]) . x )
then reconsider v1 = y as Element of the carrier of V ;
A6: [1r,y] in [:COMPLEX,D:] by A5, ZFMISC_1:87;
then ( the Mult of V | [:COMPLEX,V1:]) . [1r,y] = 1r * v1 by FUNCT_1:49
.= y by Def5 ;
hence  ex x being set st
( x in dom ( the Mult of V | [:COMPLEX,V1:]) & y = ( the Mult of V | [:COMPLEX,V1:]) . x ) by A4, A6; ::_thesis: verum
end;
given x being set  such that A7: x in dom ( the Mult of V | [:COMPLEX,V1:]) and
A8: y = ( the Mult of V | [:COMPLEX,V1:]) . x ; ::_thesis: y in D
consider x1, x2 being set  such that
A9: x1 in COMPLEX and
A10: x2 in D and
A11: x = [x1,x2] by A4, A7, ZFMISC_1:def_2;
reconsider xx1 = x1 as Element of COMPLEX by A9;
reconsider v2 = x2 as Element of the carrier of V by A10;
 [x1,x2] in [:COMPLEX,V1:] by A9, A10, ZFMISC_1:87;
then  y = xx1 * v2 by A8, A11, FUNCT_1:49;
hence  y in D by A2, A10, Def7; ::_thesis: verum
end;
then  D = rng ( the Mult of V | [:COMPLEX,V1:]) by FUNCT_1:def_3;
then reconsider M = the Mult of V | [:COMPLEX,V1:] as Function of [:COMPLEX,D:],D by A4, FUNCT_2:def_1, RELSET_1:4;
set A = the addF of V || V1;
reconsider d1 = 0. V as Element of D by A2, Th20;
 dom the addF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def_1;
then  dom ( the addF of V || V1) = [: the carrier of V, the carrier of V:] /\ [:V1,V1:] by RELAT_1:61;
then A12: dom ( the addF of V || V1) = [:D,D:] by XBOOLE_1:28, ZFMISC_1:96;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_D_implies_ex_x_being_set_st_
(_x_in_dom_(_the_addF_of_V_||_V1)_&_y_=_(_the_addF_of_V_||_V1)_._x_)_)_&_(_ex_x_being_set_st_
(_x_in_dom_(_the_addF_of_V_||_V1)_&_y_=_(_the_addF_of_V_||_V1)_._x_)_implies_y_in_D_)_)
let y be set ; ::_thesis: ( ( y in D implies ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) ) & ( ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) implies y in D ) )
thus  ( y in D implies ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) ) ::_thesis: ( ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) implies y in D )
proof
assume A13: y in D ; ::_thesis: ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x )
then reconsider v1 = y, v0 = d1 as Element of the carrier of V ;
A14: [d1,y] in [:D,D:] by A13, ZFMISC_1:87;
then ( the addF of V || V1) . [d1,y] = v0 + v1 by FUNCT_1:49
.= y by RLVECT_1:4 ;
hence  ex x being set st
( x in dom ( the addF of V || V1) & y = ( the addF of V || V1) . x ) by A12, A14; ::_thesis: verum
end;
given x being set  such that A15: x in dom ( the addF of V || V1) and
A16: y = ( the addF of V || V1) . x ; ::_thesis: y in D
consider x1, x2 being set  such that
A17: ( x1 in D & x2 in D ) and
A18: x = [x1,x2] by A12, A15, ZFMISC_1:def_2;
reconsider v1 = x1, v2 = x2 as Element of the carrier of V by A17;
 [x1,x2] in [:V1,V1:] by A17, ZFMISC_1:87;
then  y = v1 + v2 by A16, A18, FUNCT_1:49;
hence  y in D by A2, A17, Def7; ::_thesis: verum
end;
then  D = rng ( the addF of V || V1) by FUNCT_1:def_3;
then reconsider A = the addF of V || V1 as Function of [:D,D:],D by A12, FUNCT_2:def_1, RELSET_1:4;
set W = CLSStruct(# D,d1,A,M #);
 CLSStruct(# D,d1,A,M #) is Subspace of V by Th43;
hence  ex W being strict Subspace of V st V1 = the carrier of W ; ::_thesis: verum
end;

definition
let V be ComplexLinearSpace;
func (0). V ->  strict Subspace of V means :Def9: :: CLVECT_1:def 9
 the carrier of it = {(0. V)};
correctness
existence
ex b1 being strict Subspace of V st the carrier of b1 = {(0. V)};
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = {(0. V)} & the carrier of b2 = {(0. V)} holds
b1 = b2;
by Th23, Th49, Th54;
end;

:: deftheorem Def9 defines (0). CLVECT_1:def_9_:_
 for V being ComplexLinearSpace
for b2 being strict Subspace of V holds
( b2 = (0). V iff the carrier of b2 = {(0. V)} );

definition
let V be ComplexLinearSpace;
func (Omega). V ->  strict Subspace of V equals :: CLVECT_1:def 10
 CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);
coherence
 CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V
proof
set W = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);
A1: for u, v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (u + v) + w = u + (v + w)
proof
let u, v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (u + v) + w = u + (v + w)
reconsider u9 = u, v9 = v, w9 = w as VECTOR of V ;
thus (u + v) + w = (u9 + v9) + w9
.= u9 + (v9 + w9) by RLVECT_1:def_3
.= u + (v + w) ; ::_thesis: verum
end;
A2: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v
proof
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v
reconsider v9 = v as VECTOR of V ;
thus v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v9 + (0. V)
.= v by RLVECT_1:4 ; ::_thesis: verum
end;
A3: CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable
proof
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v9 = v as VECTOR of V ;
consider w9 being VECTOR of V such that
A4: v9 + w9 = 0. V by ALGSTR_0:def_11;
reconsider w = w9 as VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
thus  v + w = 0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by A4; ::_thesis: verum
end;
A5: for z1, z2 being Complex
for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (z1 * z2) * v = z1 * (z2 * v)
proof
let z1, z2 be Complex; ::_thesis: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (z1 * z2) * v = z1 * (z2 * v)
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (z1 * z2) * v = z1 * (z2 * v)
reconsider v9 = v as VECTOR of V ;
thus (z1 * z2) * v = (z1 * z2) * v9
.= z1 * (z2 * v9) by Def4
.= z1 * (z2 * v) ; ::_thesis: verum
end;
A6: for z1, z2 being Complex
for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (z1 + z2) * v = (z1 * v) + (z2 * v)
proof
let z1, z2 be Complex; ::_thesis: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (z1 + z2) * v = (z1 * v) + (z2 * v)
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: (z1 + z2) * v = (z1 * v) + (z2 * v)
reconsider v9 = v as VECTOR of V ;
thus (z1 + z2) * v = (z1 + z2) * v9
.= (z1 * v9) + (z2 * v9) by Def3
.= (z1 * v) + (z2 * v) ; ::_thesis: verum
end;
A7: for z being Complex
for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds z * (v + w) = (z * v) + (z * w)
proof
let z be Complex; ::_thesis: for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds z * (v + w) = (z * v) + (z * w)
let v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: z * (v + w) = (z * v) + (z * w)
reconsider v9 = v, w9 = w as VECTOR of V ;
thus z * (v + w) = z * (v9 + w9)
.= (z * v9) + (z * w9) by Def2
.= (z * v) + (z * w) ; ::_thesis: verum
end;
A8: for z being Complex
for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
for v9, w9 being VECTOR of V st v = v9 & w = w9 holds
( v + w = v9 + w9 & z * v = z * v9 ) ;
A9: for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + w = w + v
proof
let v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: v + w = w + v
reconsider v9 = v, w9 = w as VECTOR of V ;
thus v + w = w9 + v9 by A8
.= w + v ; ::_thesis: verum
end;
 for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds 1r * v = v
proof
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); ::_thesis: 1r * v = v
reconsider v9 = v as VECTOR of V ;
thus 1r * v = 1r * v9
.= v by Def5 ; ::_thesis: verum
end;
then reconsider W = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) as ComplexLinearSpace by A9, A1, A2, A3, A7, A6, A5, Def2, Def3, Def4, Def5, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4;
A10: the Mult of W = the Mult of V | [:COMPLEX, the carrier of W:] by RELSET_1:19;
 ( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19;
hence  CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V by A10, Def8; ::_thesis: verum
end;
end;

:: deftheorem  defines (Omega). CLVECT_1:def_10_:_
 for V being ComplexLinearSpace holds (Omega). V = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);

theorem Th55: :: CLVECT_1:55
for V being ComplexLinearSpace
for W being Subspace of V holds (0). W = (0). V
proof
let V be ComplexLinearSpace; ::_thesis: for W being Subspace of V holds (0). W = (0). V
let W be Subspace of V; ::_thesis: (0). W = (0). V
 ( the carrier of ((0). W) = {(0. W)} & the carrier of ((0). V) = {(0. V)} ) by Def9;
then A1: the carrier of ((0). W) = the carrier of ((0). V) by Def8;
 (0). W is Subspace of V by Th46;
hence  (0). W = (0). V by A1, Th49; ::_thesis: verum
end;

theorem Th56: :: CLVECT_1:56
for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds (0). W1 = (0). W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds (0). W1 = (0). W2
let W1, W2 be Subspace of V; ::_thesis: (0). W1 = (0). W2
 (0). W1 = (0). V by Th55;
hence  (0). W1 = (0). W2 by Th55; ::_thesis: verum
end;

theorem :: CLVECT_1:57
for V being ComplexLinearSpace
for W being Subspace of V holds (0). W is Subspace of V by Th46;

theorem :: CLVECT_1:58
for V being ComplexLinearSpace
for W being Subspace of V holds (0). V is Subspace of W
proof
let V be ComplexLinearSpace; ::_thesis: for W being Subspace of V holds (0). V is Subspace of W
let W be Subspace of V; ::_thesis: (0). V is Subspace of W
the carrier of ((0). V) = {(0. V)} by Def9
.= {(0. W)} by Def8 ;
hence  (0). V is Subspace of W by Th47; ::_thesis: verum
end;

theorem :: CLVECT_1:59
for V being ComplexLinearSpace
for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2
let W1, W2 be Subspace of V; ::_thesis: (0). W1 is Subspace of W2
 (0). W1 = (0). W2 by Th56;
hence  (0). W1 is Subspace of W2 ; ::_thesis: verum
end;

theorem :: CLVECT_1:60
for V being strict ComplexLinearSpace holds V is Subspace of (Omega). V ;

definition
let V be ComplexLinearSpace;
let v be VECTOR of V;
let W be Subspace of V;
funcv + W ->  Subset of V equals :: CLVECT_1:def 11
 {  (v + u) where u is VECTOR of V : u in W  }  ;
coherence
  {  (v + u) where u is VECTOR of V : u in W  }  is Subset of V
proof
set Y =  {  (v + u) where u is VECTOR of V : u in W  }  ;
defpred S1[ set ] means  ex u being VECTOR of V st
( $1 = v + u & u in W );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in the carrier of V & S1[x] ) ) from XBOOLE_0:sch_1();
 X c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of V )
assume  x in X ; ::_thesis: x in the carrier of V
hence  x in the carrier of V by A1; ::_thesis: verum
end;
then reconsider X = X as Subset of V ;
A2:  {  (v + u) where u is VECTOR of V : u in W  }  c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where u is VECTOR of V : u in W  }  or x in X )
assume  x in  {  (v + u) where u is VECTOR of V : u in W  }  ; ::_thesis: x in X
then  ex u being VECTOR of V st
( x = v + u & u in W ) ;
hence  x in X by A1; ::_thesis: verum
end;
 X c=  {  (v + u) where u is VECTOR of V : u in W  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in  {  (v + u) where u is VECTOR of V : u in W  }  )
assume  x in X ; ::_thesis: x in  {  (v + u) where u is VECTOR of V : u in W  }
then  ex u being VECTOR of V st
( x = v + u & u in W ) by A1;
hence  x in  {  (v + u) where u is VECTOR of V : u in W  }  ; ::_thesis: verum
end;
hence   {  (v + u) where u is VECTOR of V : u in W  }  is Subset of V by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem  defines + CLVECT_1:def_11_:_
 for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds v + W =  {  (v + u) where u is VECTOR of V : u in W  }  ;

Lm5:  for V being ComplexLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W
proof
let V be ComplexLinearSpace; ::_thesis: for W being Subspace of V holds (0. V) + W = the carrier of W
let W be Subspace of V; ::_thesis: (0. V) + W = the carrier of W
set A =  {  ((0. V) + u) where u is VECTOR of V : u in W  }  ;
A1: the carrier of W c=  {  ((0. V) + u) where u is VECTOR of V : u in W  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }  )
assume  x in the carrier of W ; ::_thesis: x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }
then A2: x in W by STRUCT_0:def_5;
then  x in V by Th28;
then reconsider y = x as Element of V by STRUCT_0:def_5;
 (0. V) + y = x by RLVECT_1:4;
hence  x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }  by A2; ::_thesis: verum
end;
  {  ((0. V) + u) where u is VECTOR of V : u in W  }  c= the carrier of W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }  or x in the carrier of W )
assume  x in  {  ((0. V) + u) where u is VECTOR of V : u in W  }  ; ::_thesis: x in the carrier of W
then consider u being VECTOR of V such that
A3: x = (0. V) + u and
A4: u in W ;
 x = u by A3, RLVECT_1:4;
hence  x in the carrier of W by A4, STRUCT_0:def_5; ::_thesis: verum
end;
hence  (0. V) + W = the carrier of W by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let V be ComplexLinearSpace;
let W be Subspace of V;
mode Coset of W ->  Subset of V means :Def12: :: CLVECT_1:def 12
 ex v being VECTOR of V st it = v + W;
existence
 ex b1 being Subset of V ex v being VECTOR of V st b1 = v + W
proof
reconsider VW = the carrier of W as Subset of V by Def8;
take  VW ; ::_thesis: ex v being VECTOR of V st VW = v + W
take  0. V ; ::_thesis: VW = (0. V) + W
thus  VW = (0. V) + W by Lm5; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines Coset CLVECT_1:def_12_:_
 for V being ComplexLinearSpace
for W being Subspace of V
for b3 being Subset of V holds
( b3 is Coset of W iff ex v being VECTOR of V st b3 = v + W );


theorem Th61: :: CLVECT_1:61
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( 0. V in v + W iff v in W )
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W being Subspace of V holds
( 0. V in v + W iff v in W )
let v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( 0. V in v + W iff v in W )
let W be Subspace of V; ::_thesis: ( 0. V in v + W iff v in W )
thus  ( 0. V in v + W implies v in W ) ::_thesis: ( v in W implies 0. V in v + W )
proof
assume  0. V in v + W ; ::_thesis: v in W
then consider u being VECTOR of V such that
A1: 0. V = v + u and
A2: u in W ;
 v = - u by A1, RLVECT_1:def_10;
hence  v in W by A2, Th41; ::_thesis: verum
end;
assume  v in W ; ::_thesis: 0. V in v + W
then A3: - v in W by Th41;
0. V = v - v by RLVECT_1:15
.= v + (- v) ;
hence  0. V in v + W by A3; ::_thesis: verum
end;

theorem Th62: :: CLVECT_1:62
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds v in v + W
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W being Subspace of V holds v in v + W
let v be VECTOR of V; ::_thesis: for W being Subspace of V holds v in v + W
let W be Subspace of V; ::_thesis: v in v + W
 ( v + (0. V) = v & 0. V in W ) by Th36, RLVECT_1:4;
hence  v in v + W ; ::_thesis: verum
end;

theorem :: CLVECT_1:63
for V being ComplexLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W by Lm5;

theorem Th64: :: CLVECT_1:64
for V being ComplexLinearSpace
for v being VECTOR of V holds v + ((0). V) = {v}
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V holds v + ((0). V) = {v}
let v be VECTOR of V; ::_thesis: v + ((0). V) = {v}
thus  v + ((0). V) c= {v} :: according to XBOOLE_0:def_10 ::_thesis: {v} c= v + ((0). V)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + ((0). V) or x in {v} )
assume  x in v + ((0). V) ; ::_thesis: x in {v}
then consider u being VECTOR of V such that
A1: x = v + u and
A2: u in (0). V ;
A3: the carrier of ((0). V) = {(0. V)} by Def9;
 u in the carrier of ((0). V) by A2, STRUCT_0:def_5;
then  u = 0. V by A3, TARSKI:def_1;
then  x = v by A1, RLVECT_1:4;
hence  x in {v} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in v + ((0). V) )
assume  x in {v} ; ::_thesis: x in v + ((0). V)
then A4: x = v by TARSKI:def_1;
 ( 0. V in (0). V & v = v + (0. V) ) by Th36, RLVECT_1:4;
hence  x in v + ((0). V) by A4; ::_thesis: verum
end;

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 )
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
let v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
let W be Subspace of V; ::_thesis: ( v in W iff v + W = the carrier of W )
 ( 0. V in W & v + (0. V) = v ) by Th36, RLVECT_1:4;
then A1: v in  {  (v + u) where u is VECTOR of V : u in W  }  ;
thus  ( v in W implies v + W = the carrier of W ) ::_thesis: ( v + W = the carrier of W implies v in W )
proof
assume A2: v in W ; ::_thesis: v + W = the carrier of W
thus  v + W c= the carrier of W :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W c= v + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in the carrier of W )
assume  x in v + W ; ::_thesis: x in the carrier of W
then consider u being VECTOR of V such that
A3: x = v + u and
A4: u in W ;
 v + u in W by A2, A4, Th39;
hence  x in the carrier of W by A3, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in v + W )
assume  x in the carrier of W ; ::_thesis: x in v + W
then reconsider y = x, z = v as Element of W by A2, STRUCT_0:def_5;
reconsider y1 = y, z1 = z as VECTOR of V by Th29;
A5: z + (y - z) = (y + z) - z by RLVECT_1:def_3
.= y + (z - z) by RLVECT_1:def_3
.= y + (0. W) by RLVECT_1:15
.= x by RLVECT_1:4 ;
 y - z in W by STRUCT_0:def_5;
then A6: y1 - z1 in W by Th35;
 y - z = y1 - z1 by Th35;
then  z1 + (y1 - z1) = x by A5, Th32;
hence  x in v + W by A6; ::_thesis: verum
end;
assume A7: v + W = the carrier of W ; ::_thesis: v in W
assume  not v in W ; ::_thesis: contradiction
hence  contradiction by A7, A1, STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th65: :: CLVECT_1:65
for V being ComplexLinearSpace
for v being VECTOR of V holds v + ((Omega). V) = the carrier of V
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V holds v + ((Omega). V) = the carrier of V
let v be VECTOR of V; ::_thesis: v + ((Omega). V) = the carrier of V
 v in (Omega). V by STRUCT_0:def_5;
hence  v + ((Omega). V) = the carrier of V by Lm6; ::_thesis: verum
end;

theorem Th66: :: CLVECT_1:66
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( 0. V in v + W iff v + W = the carrier of W )
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W being Subspace of V holds
( 0. V in v + W iff v + W = the carrier of W )
let v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( 0. V in v + W iff v + W = the carrier of W )
let W be Subspace of V; ::_thesis: ( 0. V in v + W iff v + W = the carrier of W )
 ( 0. V in v + W iff v in W ) by Th61;
hence  ( 0. V in v + W iff v + W = the carrier of W ) by Lm6; ::_thesis: verum
end;

theorem :: CLVECT_1:67
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 ) by Lm6;

theorem Th68: :: CLVECT_1:68
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
(z * v) + W = the carrier of W
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
(z * v) + W = the carrier of W
let v be VECTOR of V; ::_thesis: for z being Complex
for W being Subspace of V st v in W holds
(z * v) + W = the carrier of W
let z be Complex; ::_thesis: for W being Subspace of V st v in W holds
(z * v) + W = the carrier of W
let W be Subspace of V; ::_thesis: ( v in W implies (z * v) + W = the carrier of W )
assume A1: v in W ; ::_thesis: (z * v) + W = the carrier of W
thus  (z * v) + W c= the carrier of W :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W c= (z * v) + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (z * v) + W or x in the carrier of W )
assume  x in (z * v) + W ; ::_thesis: x in the carrier of W
then consider u being VECTOR of V such that
A2: x = (z * v) + u and
A3: u in W ;
 z * v in W by A1, Th40;
then  (z * v) + u in W by A3, Th39;
hence  x in the carrier of W by A2, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W or x in (z * v) + W )
assume A4: x in the carrier of W ; ::_thesis: x in (z * v) + W
then A5: x in W by STRUCT_0:def_5;
 the carrier of W c= the carrier of V by Def8;
then reconsider y = x as Element of V by A4;
A6: (z * v) + (y - (z * v)) = (y + (z * v)) - (z * v) by RLVECT_1:def_3
.= y + ((z * v) - (z * v)) by RLVECT_1:def_3
.= y + (0. V) by RLVECT_1:15
.= x by RLVECT_1:4 ;
 z * v in W by A1, Th40;
then  y - (z * v) in W by A5, Th42;
hence  x in (z * v) + W by A6; ::_thesis: verum
end;

theorem Th69: :: CLVECT_1:69
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds
v in W
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds
v in W
let v be VECTOR of V; ::_thesis: for z being Complex
for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds
v in W
let z be Complex; ::_thesis: for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds
v in W
let W be Subspace of V; ::_thesis: ( z <> 0 & (z * v) + W = the carrier of W implies v in W )
assume that
A1: z <> 0 and
A2: (z * v) + W = the carrier of W ; ::_thesis: v in W
assume  not v in W ; ::_thesis: contradiction
then  not 1r * v in W by Def5;
then  not ((z ") * z) * v in W by A1, XCMPLX_0:def_7;
then  not (z ") * (z * v) in W by Def4;
then A3: not z * v in W by Th40;
 ( 0. V in W & (z * v) + (0. V) = z * v ) by Th36, RLVECT_1:4;
then  z * v in  {  ((z * v) + u) where u is VECTOR of V : u in W  }  ;
hence  contradiction by A2, A3, STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th70: :: CLVECT_1:70
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 )
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W being Subspace of V holds
( v in W iff (- v) + W = the carrier of W )
let v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( v in W iff (- v) + W = the carrier of W )
let W be Subspace of V; ::_thesis: ( v in W iff (- v) + W = the carrier of W )
 ( v in W iff ((- 1r) * v) + W = the carrier of W ) by Th68, Th69;
hence  ( v in W iff (- v) + W = the carrier of W ) by Th3; ::_thesis: verum
end;

theorem Th71: :: CLVECT_1:71
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in W iff v + W = (v + u) + W )
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V holds
( u in W iff v + W = (v + u) + W )
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( u in W iff v + W = (v + u) + W )
let W be Subspace of V; ::_thesis: ( u in W iff v + W = (v + u) + W )
thus  ( u in W implies v + W = (v + u) + W ) ::_thesis: ( v + W = (v + u) + W implies u in W )
proof
assume A1: u in W ; ::_thesis: v + W = (v + u) + W
thus  v + W c= (v + u) + W :: according to XBOOLE_0:def_10 ::_thesis: (v + u) + W c= v + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in (v + u) + W )
assume  x in v + W ; ::_thesis: x in (v + u) + W
then consider v1 being VECTOR of V such that
A2: x = v + v1 and
A3: v1 in W ;
A4: (v + u) + (v1 - u) = v + (u + (v1 - u)) by RLVECT_1:def_3
.= v + ((v1 + u) - u) by RLVECT_1:def_3
.= v + (v1 + (u - u)) by RLVECT_1:def_3
.= v + (v1 + (0. V)) by RLVECT_1:15
.= x by A2, RLVECT_1:4 ;
 v1 - u in W by A1, A3, Th42;
hence  x in (v + u) + W by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (v + u) + W or x in v + W )
assume  x in (v + u) + W ; ::_thesis: x in v + W
then consider v2 being VECTOR of V such that
A5: x = (v + u) + v2 and
A6: v2 in W ;
A7: x = v + (u + v2) by A5, RLVECT_1:def_3;
 u + v2 in W by A1, A6, Th39;
hence  x in v + W by A7; ::_thesis: verum
end;
assume A8: v + W = (v + u) + W ; ::_thesis: u in W
 ( 0. V in W & v + (0. V) = v ) by Th36, RLVECT_1:4;
then  v in (v + u) + W by A8;
then consider u1 being VECTOR of V such that
A9: v = (v + u) + u1 and
A10: u1 in W ;
 ( v = v + (0. V) & v = v + (u + u1) ) by A9, RLVECT_1:4, RLVECT_1:def_3;
then  u + u1 = 0. V by RLVECT_1:8;
then  u = - u1 by RLVECT_1:def_10;
hence  u in W by A10, Th41; ::_thesis: verum
end;

theorem :: CLVECT_1:72
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in W iff v + W = (v - u) + W )
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V holds
( u in W iff v + W = (v - u) + W )
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( u in W iff v + W = (v - u) + W )
let W be Subspace of V; ::_thesis: ( u in W iff v + W = (v - u) + W )
A1: ( - u in W implies u in W )
proof
assume  - u in W ; ::_thesis: u in W
then  - (- u) in W by Th41;
hence  u in W by RLVECT_1:17; ::_thesis: verum
end;
 ( - u in W iff v + W = (v + (- u)) + W ) by Th71;
hence  ( u in W iff v + W = (v - u) + W ) by A1, Th41; ::_thesis: verum
end;

theorem Th73: :: CLVECT_1:73
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V holds
( v in u + W iff u + W = v + W )
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for W being Subspace of V holds
( v in u + W iff u + W = v + W )
let v, u be VECTOR of V; ::_thesis: for W being Subspace of V holds
( v in u + W iff u + W = v + W )
let W be Subspace of V; ::_thesis: ( v in u + W iff u + W = v + W )
thus  ( v in u + W implies u + W = v + W ) ::_thesis: ( u + W = v + W implies v in u + W )
proof
assume  v in u + W ; ::_thesis: u + W = v + W
then consider z being VECTOR of V such that
A1: v = u + z and
A2: z in W ;
thus  u + W c= v + W :: according to XBOOLE_0:def_10 ::_thesis: v + W c= u + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in u + W or x in v + W )
assume  x in u + W ; ::_thesis: x in v + W
then consider v1 being VECTOR of V such that
A3: x = u + v1 and
A4: v1 in W ;
v - z = u + (z - z) by A1, RLVECT_1:def_3
.= u + (0. V) by RLVECT_1:15
.= u by RLVECT_1:4 ;
then A5: x = v + (v1 + (- z)) by A3, RLVECT_1:def_3
.= v + (v1 - z) ;
 v1 - z in W by A2, A4, Th42;
hence  x in v + W by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W or x in u + W )
assume  x in v + W ; ::_thesis: x in u + W
then consider v2 being VECTOR of V such that
A6: ( x = v + v2 & v2 in W ) ;
 ( z + v2 in W & x = u + (z + v2) ) by A1, A2, A6, Th39, RLVECT_1:def_3;
hence  x in u + W ; ::_thesis: verum
end;
thus  ( u + W = v + W implies v in u + W ) by Th62; ::_thesis: verum
end;

theorem Th74: :: CLVECT_1:74
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v + W = (- v) + W iff v in W )
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W being Subspace of V holds
( v + W = (- v) + W iff v in W )
let v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( v + W = (- v) + W iff v in W )
let W be Subspace of V; ::_thesis: ( v + W = (- v) + W iff v in W )
thus  ( v + W = (- v) + W implies v in W ) ::_thesis: ( v in W implies v + W = (- v) + W )
proof
assume  v + W = (- v) + W ; ::_thesis: v in W
then  v in (- v) + W by Th62;
then consider u being VECTOR of V such that
A1: v = (- v) + u and
A2: u in W ;
0. V = v - ((- v) + u) by A1, RLVECT_1:15
.= (v - (- v)) - u by RLVECT_1:27
.= (v + v) - u by RLVECT_1:17
.= ((1r * v) + v) - u by Def5
.= ((1r * v) + (1r * v)) - u by Def5
.= ((1r + 1r) * v) - u by Def3 ;
then  ((1r + 1r) ") * ((1r + 1r) * v) = ((1r + 1r) ") * u by RLVECT_1:21;
then  (((1r + 1r) ") * (1r + 1r)) * v = ((1r + 1r) ") * u by Def4;
then  v = ((1r + 1r) ") * u by Def5;
hence  v in W by A2, Th40; ::_thesis: verum
end;
assume A3: v in W ; ::_thesis: v + W = (- v) + W
then  v + W = the carrier of W by Lm6;
hence  v + W = (- v) + W by A3, Th70; ::_thesis: verum
end;

theorem Th75: :: CLVECT_1:75
for V being ComplexLinearSpace
for u, v1, v2 being VECTOR of V
for W being Subspace of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
proof
let V be ComplexLinearSpace; ::_thesis: for u, v1, v2 being VECTOR of V
for W being Subspace of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
let u, v1, v2 be VECTOR of V; ::_thesis: for W being Subspace of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W
let W be Subspace of V; ::_thesis: ( u in v1 + W & u in v2 + W implies v1 + W = v2 + W )
assume that
A1: u in v1 + W and
A2: u in v2 + W ; ::_thesis: v1 + W = v2 + W
consider x1 being VECTOR of V such that
A3: u = v1 + x1 and
A4: x1 in W by A1;
consider x2 being VECTOR of V such that
A5: u = v2 + x2 and
A6: x2 in W by A2;
thus  v1 + W c= v2 + W :: according to XBOOLE_0:def_10 ::_thesis: v2 + W c= v1 + W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v1 + W or x in v2 + W )
assume  x in v1 + W ; ::_thesis: x in v2 + W
then consider u1 being VECTOR of V such that
A7: x = v1 + u1 and
A8: u1 in W ;
 x2 - x1 in W by A4, A6, Th42;
then A9: (x2 - x1) + u1 in W by A8, Th39;
u - x1 = v1 + (x1 - x1) by A3, RLVECT_1:def_3
.= v1 + (0. V) by RLVECT_1:15
.= v1 by RLVECT_1:4 ;
then x = (v2 + (x2 - x1)) + u1 by A5, A7, RLVECT_1:def_3
.= v2 + ((x2 - x1) + u1) by RLVECT_1:def_3 ;
hence  x in v2 + W by A9; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v2 + W or x in v1 + W )
assume  x in v2 + W ; ::_thesis: x in v1 + W
then consider u1 being VECTOR of V such that
A10: x = v2 + u1 and
A11: u1 in W ;
 x1 - x2 in W by A4, A6, Th42;
then A12: (x1 - x2) + u1 in W by A11, Th39;
u - x2 = v2 + (x2 - x2) by A5, RLVECT_1:def_3
.= v2 + (0. V) by RLVECT_1:15
.= v2 by RLVECT_1:4 ;
then x = (v1 + (x1 - x2)) + u1 by A3, A10, RLVECT_1:def_3
.= v1 + ((x1 - x2) + u1) by RLVECT_1:def_3 ;
hence  x in v1 + W by A12; ::_thesis: verum
end;

theorem :: CLVECT_1:76
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in v + W & u in (- v) + W holds
v in W
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V st u in v + W & u in (- v) + W holds
v in W
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V st u in v + W & u in (- v) + W holds
v in W
let W be Subspace of V; ::_thesis: ( u in v + W & u in (- v) + W implies v in W )
assume  ( u in v + W & u in (- v) + W ) ; ::_thesis: v in W
then  v + W = (- v) + W by Th75;
hence  v in W by Th74; ::_thesis: verum
end;

theorem Th77: :: CLVECT_1:77
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st z <> 1r & z * v in v + W holds
v in W
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st z <> 1r & z * v in v + W holds
v in W
let v be VECTOR of V; ::_thesis: for z being Complex
for W being Subspace of V st z <> 1r & z * v in v + W holds
v in W
let z be Complex; ::_thesis: for W being Subspace of V st z <> 1r & z * v in v + W holds
v in W
let W be Subspace of V; ::_thesis: ( z <> 1r & z * v in v + W implies v in W )
assume that
A1: z <> 1r and
A2: z * v in v + W ; ::_thesis: v in W
A3: z - 1r <> 0 by A1;
consider u being VECTOR of V such that
A4: z * v = v + u and
A5: u in W by A2;
u = u + (0. V) by RLVECT_1:4
.= u + (v - v) by RLVECT_1:15
.= (z * v) - v by A4, RLVECT_1:def_3
.= (z * v) - (1r * v) by Def5
.= (z - 1r) * v by Th10 ;
then  ((z - 1r) ") * u = (((z - 1r) ") * (z - 1r)) * v by Def4;
then  1r * v = ((z - 1r) ") * u by A3, XCMPLX_0:def_7;
then  v = ((z - 1r) ") * u by Def5;
hence  v in W by A5, Th40; ::_thesis: verum
end;

theorem Th78: :: CLVECT_1:78
for V being ComplexLinearSpace
for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
z * v in v + W
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
z * v in v + W
let v be VECTOR of V; ::_thesis: for z being Complex
for W being Subspace of V st v in W holds
z * v in v + W
let z be Complex; ::_thesis: for W being Subspace of V st v in W holds
z * v in v + W
let W be Subspace of V; ::_thesis: ( v in W implies z * v in v + W )
assume  v in W ; ::_thesis: z * v in v + W
then A1: (z - 1r) * v in W by Th40;
z * v = ((z - 1r) + 1r) * v
.= ((z - 1r) * v) + (1r * v) by Def3
.= v + ((z - 1r) * v) by Def5 ;
hence  z * v in v + W by A1; ::_thesis: verum
end;

theorem :: CLVECT_1:79
for V being ComplexLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( - v in v + W iff v in W )
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W being Subspace of V holds
( - v in v + W iff v in W )
let v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( - v in v + W iff v in W )
let W be Subspace of V; ::_thesis: ( - v in v + W iff v in W )
 (- 1r) * v = - v by Th3;
hence  ( - v in v + W iff v in W ) by Th77, Th78; ::_thesis: verum
end;

theorem Th80: :: CLVECT_1:80
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u + v in v + W iff u in W )
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V holds
( u + v in v + W iff u in W )
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( u + v in v + W iff u in W )
let W be Subspace of V; ::_thesis: ( u + v in v + W iff u in W )
thus  ( u + v in v + W implies u in W ) ::_thesis: ( u in W implies u + v in v + W )
proof
assume  u + v in v + W ; ::_thesis: u in W
then  ex v1 being VECTOR of V st
( u + v = v + v1 & v1 in W ) ;
hence  u in W by RLVECT_1:8; ::_thesis: verum
end;
assume  u in W ; ::_thesis: u + v in v + W
hence  u + v in v + W ; ::_thesis: verum
end;

theorem :: CLVECT_1:81
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V holds
( v - u in v + W iff u in W )
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for W being Subspace of V holds
( v - u in v + W iff u in W )
let v, u be VECTOR of V; ::_thesis: for W being Subspace of V holds
( v - u in v + W iff u in W )
let W be Subspace of V; ::_thesis: ( v - u in v + W iff u in W )
A1: v - u = (- u) + v ;
A2: ( - u in W implies - (- u) in W ) by Th41;
 ( u in W implies - u in W ) by Th41;
hence  ( v - u in v + W iff u in W ) by A1, A2, Th80, RLVECT_1:17; ::_thesis: verum
end;

theorem Th82: :: CLVECT_1:82
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
let W be Subspace of V; ::_thesis: ( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )
thus  ( u in v + W implies ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) ) ::_thesis: ( ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) implies u in v + W )
proof
assume  u in v + W ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & u = v + v1 )
then  ex v1 being VECTOR of V st
( u = v + v1 & v1 in W ) ;
hence  ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) ; ::_thesis: verum
end;
given v1 being VECTOR of V such that A1: ( v1 in W & u = v + v1 ) ; ::_thesis: u in v + W
thus  u in v + W by A1; ::_thesis: verum
end;

theorem :: CLVECT_1:83
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
let W be Subspace of V; ::_thesis: ( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )
thus  ( u in v + W implies ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) ) ::_thesis: ( ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) implies u in v + W )
proof
assume  u in v + W ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & u = v - v1 )
then consider v1 being VECTOR of V such that
A1: u = v + v1 and
A2: v1 in W ;
take x = - v1; ::_thesis: ( x in W & u = v - x )
thus  x in W by A2, Th41; ::_thesis: u = v - x
thus  u = v - x by A1, RLVECT_1:17; ::_thesis: verum
end;
given v1 being VECTOR of V such that A3: v1 in W and
A4: u = v - v1 ; ::_thesis: u in v + W
 - v1 in W by A3, Th41;
hence  u in v + W by A4; ::_thesis: verum
end;

theorem Th84: :: CLVECT_1:84
for V being ComplexLinearSpace
for v1, v2 being VECTOR of V
for W being Subspace of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
proof
let V be ComplexLinearSpace; ::_thesis: for v1, v2 being VECTOR of V
for W being Subspace of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
let v1, v2 be VECTOR of V; ::_thesis: for W being Subspace of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
let W be Subspace of V; ::_thesis: ( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
thus  ( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) implies v1 - v2 in W ) ::_thesis: ( v1 - v2 in W implies ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) )
proof
given v being VECTOR of V such that A1: v1 in v + W and
A2: v2 in v + W ; ::_thesis: v1 - v2 in W
consider u2 being VECTOR of V such that
A3: u2 in W and
A4: v2 = v + u2 by A2, Th82;
consider u1 being VECTOR of V such that
A5: u1 in W and
A6: v1 = v + u1 by A1, Th82;
v1 - v2 = (u1 + v) + ((- v) - u2) by A6, A4, RLVECT_1:30
.= ((u1 + v) + (- v)) - u2 by RLVECT_1:def_3
.= (u1 + (v + (- v))) - u2 by RLVECT_1:def_3
.= (u1 + (0. V)) - u2 by RLVECT_1:5
.= u1 - u2 by RLVECT_1:4 ;
hence  v1 - v2 in W by A5, A3, Th42; ::_thesis: verum
end;
assume  v1 - v2 in W ; ::_thesis: ex v being VECTOR of V st
( v1 in v + W & v2 in v + W )
then A7: - (v1 - v2) in W by Th41;
take  v1 ; ::_thesis: ( v1 in v1 + W & v2 in v1 + W )
thus  v1 in v1 + W by Th62; ::_thesis: v2 in v1 + W
v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by RLVECT_1:33
.= (v1 + (- v1)) + v2 by RLVECT_1:def_3
.= (0. V) + v2 by RLVECT_1:5
.= v2 by RLVECT_1:4 ;
hence  v2 in v1 + W by A7; ::_thesis: verum
end;

theorem Th85: :: CLVECT_1:85
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
let v, u be VECTOR of V; ::_thesis: for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
let W be Subspace of V; ::_thesis: ( v + W = u + W implies ex v1 being VECTOR of V st
( v1 in W & v + v1 = u ) )
assume  v + W = u + W ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )
then  v in u + W by Th62;
then consider u1 being VECTOR of V such that
A1: v = u + u1 and
A2: u1 in W ;
take v1 = u - v; ::_thesis: ( v1 in W & v + v1 = u )
0. V = (u + u1) - v by A1, RLVECT_1:15
.= u1 + (u - v) by RLVECT_1:def_3 ;
then  v1 = - u1 by RLVECT_1:def_10;
hence  v1 in W by A2, Th41; ::_thesis: v + v1 = u
thus v + v1 = (u + v) - v by RLVECT_1:def_3
.= u + (v - v) by RLVECT_1:def_3
.= u + (0. V) by RLVECT_1:15
.= u by RLVECT_1:4 ; ::_thesis: verum
end;

theorem Th86: :: CLVECT_1:86
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
let v, u be VECTOR of V; ::_thesis: for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
let W be Subspace of V; ::_thesis: ( v + W = u + W implies ex v1 being VECTOR of V st
( v1 in W & v - v1 = u ) )
assume  v + W = u + W ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )
then  u in v + W by Th62;
then consider u1 being VECTOR of V such that
A1: u = v + u1 and
A2: u1 in W ;
take v1 = v - u; ::_thesis: ( v1 in W & v - v1 = u )
0. V = (v + u1) - u by A1, RLVECT_1:15
.= u1 + (v - u) by RLVECT_1:def_3 ;
then  v1 = - u1 by RLVECT_1:def_10;
hence  v1 in W by A2, Th41; ::_thesis: v - v1 = u
thus v - v1 = (v - v) + u by RLVECT_1:29
.= (0. V) + u by RLVECT_1:15
.= u by RLVECT_1:4 ; ::_thesis: verum
end;

theorem Th87: :: CLVECT_1:87
for V being ComplexLinearSpace
for v being VECTOR of V
for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V
for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )
let v be VECTOR of V; ::_thesis: for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )
let W1, W2 be strict Subspace of V; ::_thesis: ( v + W1 = v + W2 iff W1 = W2 )
thus  ( v + W1 = v + W2 implies W1 = W2 ) ::_thesis: ( W1 = W2 implies v + W1 = v + W2 )
proof
assume A1: v + W1 = v + W2 ; ::_thesis: W1 = W2
 the carrier of W1 = the carrier of W2
proof
A2: the carrier of W1 c= the carrier of V by Def8;
thus  the carrier of W1 c= the carrier of W2 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W2 c= the carrier of W1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of W2 )
assume A3: x in the carrier of W1 ; ::_thesis: x in the carrier of W2
then reconsider y = x as Element of V by A2;
set z = v + y;
 x in W1 by A3, STRUCT_0:def_5;
then  v + y in v + W2 by A1;
then consider u being VECTOR of V such that
A4: v + y = v + u and
A5: u in W2 ;
 y = u by A4, RLVECT_1:8;
hence  x in the carrier of W2 by A5, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W2 or x in the carrier of W1 )
assume A6: x in the carrier of W2 ; ::_thesis: x in the carrier of W1
 the carrier of W2 c= the carrier of V by Def8;
then reconsider y = x as Element of V by A6;
set z = v + y;
 x in W2 by A6, STRUCT_0:def_5;
then  v + y in v + W1 by A1;
then consider u being VECTOR of V such that
A7: v + y = v + u and
A8: u in W1 ;
 y = u by A7, RLVECT_1:8;
hence  x in the carrier of W1 by A8, STRUCT_0:def_5; ::_thesis: verum
end;
hence  W1 = W2 by Th49; ::_thesis: verum
end;
thus  ( W1 = W2 implies v + W1 = v + W2 ) ; ::_thesis: verum
end;

theorem Th88: :: CLVECT_1:88
for V being ComplexLinearSpace
for v, u being VECTOR of V
for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2
proof
let V be ComplexLinearSpace; ::_thesis: for v, u being VECTOR of V
for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2
let v, u be VECTOR of V; ::_thesis: for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2
let W1, W2 be strict Subspace of V; ::_thesis: ( v + W1 = u + W2 implies W1 = W2 )
assume A1: v + W1 = u + W2 ; ::_thesis: W1 = W2
set V2 = the carrier of W2;
set V1 = the carrier of W1;
assume A2: W1 <> W2 ; ::_thesis: contradiction
A3: now__::_thesis:_not_the_carrier_of_W1_\_the_carrier_of_W2_<>_{}
set x = the Element of the carrier of W1 \ the carrier of W2;
assume  the carrier of W1 \ the carrier of W2 <> {} ; ::_thesis: contradiction
then  the Element of the carrier of W1 \ the carrier of W2 in the carrier of W1 by XBOOLE_0:def_5;
then A4: the Element of the carrier of W1 \ the carrier of W2 in W1 by STRUCT_0:def_5;
then  the Element of the carrier of W1 \ the carrier of W2 in V by Th28;
then reconsider x = the Element of the carrier of W1 \ the carrier of W2 as Element of V by STRUCT_0:def_5;
set z = v + x;
 v + x in u + W2 by A1, A4;
then consider u1 being VECTOR of V such that
A5: v + x = u + u1 and
A6: u1 in W2 ;
x = (0. V) + x by RLVECT_1:4
.= (v - v) + x by RLVECT_1:15
.= (- v) + (u + u1) by A5, RLVECT_1:def_3 ;
then A7: (v + ((- v) + (u + u1))) + W1 = v + W1 by A4, Th71;
v + ((- v) + (u + u1)) = (v - v) + (u + u1) by RLVECT_1:def_3
.= (0. V) + (u + u1) by RLVECT_1:15
.= u + u1 by RLVECT_1:4 ;
then  (u + u1) + W2 = (u + u1) + W1 by A1, A6, A7, Th71;
hence  contradiction by A2, Th87; ::_thesis: verum
end;
A8: now__::_thesis:_not_the_carrier_of_W2_\_the_carrier_of_W1_<>_{}
set x = the Element of the carrier of W2 \ the carrier of W1;
assume  the carrier of W2 \ the carrier of W1 <> {} ; ::_thesis: contradiction
then  the Element of the carrier of W2 \ the carrier of W1 in the carrier of W2 by XBOOLE_0:def_5;
then A9: the Element of the carrier of W2 \ the carrier of W1 in W2 by STRUCT_0:def_5;
then  the Element of the carrier of W2 \ the carrier of W1 in V by Th28;
then reconsider x = the Element of the carrier of W2 \ the carrier of W1 as Element of V by STRUCT_0:def_5;
set z = u + x;
 u + x in v + W1 by A1, A9;
then consider u1 being VECTOR of V such that
A10: u + x = v + u1 and
A11: u1 in W1 ;
x = (0. V) + x by RLVECT_1:4
.= (u - u) + x by RLVECT_1:15
.= (- u) + (v + u1) by A10, RLVECT_1:def_3 ;
then A12: (u + ((- u) + (v + u1))) + W2 = u + W2 by A9, Th71;
u + ((- u) + (v + u1)) = (u - u) + (v + u1) by RLVECT_1:def_3
.= (0. V) + (v + u1) by RLVECT_1:15
.= v + u1 by RLVECT_1:4 ;
then  (v + u1) + W1 = (v + u1) + W2 by A1, A11, A12, Th71;
hence  contradiction by A2, Th87; ::_thesis: verum
end;
 the carrier of W1 <> the carrier of W2 by A2, Th49;
then  ( not the carrier of W1 c= the carrier of W2 or not the carrier of W2 c= the carrier of W1 ) by XBOOLE_0:def_10;
hence  contradiction by A3, A8, XBOOLE_1:37; ::_thesis: verum
end;

theorem :: CLVECT_1:89
for V being ComplexLinearSpace
for W being Subspace of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
proof
let V be ComplexLinearSpace; ::_thesis: for W being Subspace of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
let W be Subspace of V; ::_thesis: for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )
let C be Coset of W; ::_thesis: ( C is linearly-closed iff C = the carrier of W )
thus  ( C is linearly-closed implies C = the carrier of W ) ::_thesis: ( C = the carrier of W implies C is linearly-closed )
proof
assume A1: C is linearly-closed ; ::_thesis: C = the carrier of W
consider v being VECTOR of V such that
A2: C = v + W by Def12;
 C <> {} by A2, Th62;
then  0. V in v + W by A1, A2, Th20;
hence  C = the carrier of W by A2, Th66; ::_thesis: verum
end;
thus  ( C = the carrier of W implies C is linearly-closed ) by Lm3; ::_thesis: verum
end;

theorem :: CLVECT_1:90
for V being ComplexLinearSpace
for W1, W2 being strict Subspace of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
proof
let V be ComplexLinearSpace; ::_thesis: for W1, W2 being strict Subspace of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
let W1, W2 be strict Subspace of V; ::_thesis: for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 st C1 = C2 holds
W1 = W2
let C2 be Coset of W2; ::_thesis: ( C1 = C2 implies W1 = W2 )
 ( ex v1 being VECTOR of V st C1 = v1 + W1 & ex v2 being VECTOR of V st C2 = v2 + W2 ) by Def12;
hence  ( C1 = C2 implies W1 = W2 ) by Th88; ::_thesis: verum
end;

theorem :: CLVECT_1:91
for V being ComplexLinearSpace
for v being VECTOR of V holds {v} is Coset of (0). V
proof
let V be ComplexLinearSpace; ::_thesis: for v being VECTOR of V holds {v} is Coset of (0). V
let v be VECTOR of V; ::_thesis: {v} is Coset of (0). V
 v + ((0). V) = {v} by Th64;
hence  {v} is Coset of (0). V by Def12; ::_thesis: verum
end;

theorem :: CLVECT_1:92
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being VECTOR of V st V1 = {v}
proof
let V be ComplexLinearSpace; ::_thesis: for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being VECTOR of V st V1 = {v}
let V1 be Subset of V; ::_thesis: ( V1 is Coset of (0). V implies ex v being VECTOR of V st V1 = {v} )
assume  V1 is Coset of (0). V ; ::_thesis: ex v being VECTOR of V st V1 = {v}
then consider v being VECTOR of V such that
A1: V1 = v + ((0). V) by Def12;
take  v ; ::_thesis: V1 = {v}
thus  V1 = {v} by A1, Th64; ::_thesis: verum
end;

theorem :: CLVECT_1:93
for V being ComplexLinearSpace
for W being Subspace of V holds the carrier of W is Coset of W
proof
let V be ComplexLinearSpace; ::_thesis: for W being Subspace of V holds the carrier of W is Coset of W
let W be Subspace of V; ::_thesis: the carrier of W is Coset of W
 the carrier of W = (0. V) + W by Lm5;
hence  the carrier of W is Coset of W by Def12; ::_thesis: verum
end;

theorem :: CLVECT_1:94
for V being ComplexLinearSpace holds the carrier of V is Coset of (Omega). V
proof
let V be ComplexLinearSpace; ::_thesis: the carrier of V is Coset of (Omega). V
set v = the VECTOR of V;
 ( the carrier of V is Subset of V iff the carrier of V c= the carrier of V ) ;
then reconsider A = the carrier of V as Subset of V ;
 A = the VECTOR of V + ((Omega). V) by Th65;
hence  the carrier of V is Coset of (Omega). V by Def12; ::_thesis: verum
end;

theorem :: CLVECT_1:95
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V
proof
let V be ComplexLinearSpace; ::_thesis: for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V
let V1 be Subset of V; ::_thesis: ( V1 is Coset of (Omega). V implies V1 = the carrier of V )
assume  V1 is Coset of (Omega). V ; ::_thesis: V1 = the carrier of V
then  ex v being VECTOR of V st V1 = v + ((Omega). V) by Def12;
hence  V1 = the carrier of V by Th65; ::_thesis: verum
end;

theorem :: CLVECT_1:96
for V being ComplexLinearSpace
for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
proof
let V be ComplexLinearSpace; ::_thesis: for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
let W be Subspace of V; ::_thesis: for C being Coset of W holds
( 0. V in C iff C = the carrier of W )
let C be Coset of W; ::_thesis: ( 0. V in C iff C = the carrier of W )
 ex v being VECTOR of V st C = v + W by Def12;
hence  ( 0. V in C iff C = the carrier of W ) by Th66; ::_thesis: verum
end;

theorem Th97: :: CLVECT_1:97
for V being ComplexLinearSpace
for u being VECTOR of V
for W being Subspace of V
for C being Coset of W holds
( u in C iff C = u + W )
proof
let V be ComplexLinearSpace; ::_thesis: for u being VECTOR of V
for W being Subspace of V
for C being Coset of W holds
( u in C iff C = u + W )
let u be VECTOR of V; ::_thesis: for W being Subspace of V
for C being Coset of W holds
( u in C iff C = u + W )
let W be Subspace of V; ::_thesis: for C being Coset of W holds
( u in C iff C = u + W )
let C be Coset of W; ::_thesis: ( u in C iff C = u + W )
thus  ( u in C implies C = u + W ) ::_thesis: ( C = u + W implies u in C )
proof
assume A1: u in C ; ::_thesis: C = u + W
 ex v being VECTOR of V st C = v + W by Def12;
hence  C = u + W by A1, Th73; ::_thesis: verum
end;
thus  ( C = u + W implies u in C ) by Th62; ::_thesis: verum
end;

theorem :: CLVECT_1:98
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
let W be Subspace of V; ::_thesis: for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
let C be Coset of W; ::_thesis: ( u in C & v in C implies ex v1 being VECTOR of V st
( v1 in W & u + v1 = v ) )
assume  ( u in C & v in C ) ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )
then  ( C = u + W & C = v + W ) by Th97;
hence  ex v1 being VECTOR of V st
( v1 in W & u + v1 = v ) by Th85; ::_thesis: verum
end;

theorem :: CLVECT_1:99
for V being ComplexLinearSpace
for u, v being VECTOR of V
for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
proof
let V be ComplexLinearSpace; ::_thesis: for u, v being VECTOR of V
for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
let u, v be VECTOR of V; ::_thesis: for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
let W be Subspace of V; ::_thesis: for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
let C be Coset of W; ::_thesis: ( u in C & v in C implies ex v1 being VECTOR of V st
( v1 in W & u - v1 = v ) )
assume  ( u in C & v in C ) ; ::_thesis: ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )
then  ( C = u + W & C = v + W ) by Th97;
hence  ex v1 being VECTOR of V st
( v1 in W & u - v1 = v ) by Th86; ::_thesis: verum
end;

theorem :: CLVECT_1:100
for V being ComplexLinearSpace
for v1, v2 being VECTOR of V
for W being Subspace of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
proof
let V be ComplexLinearSpace; ::_thesis: for v1, v2 being VECTOR of V
for W being Subspace of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let v1, v2 be VECTOR of V; ::_thesis: for W being Subspace of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
let W be Subspace of V; ::_thesis: ( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )
thus  ( ex C being Coset of W st
( v1 in C & v2 in C ) implies v1 - v2 in W ) ::_thesis: ( v1 - v2 in W implies ex C being Coset of W st
( v1 in C & v2 in C ) )
proof
given C being Coset of W such that A1: ( v1 in C & v2 in C ) ; ::_thesis: v1 - v2 in W
 ex v being VECTOR of V st C = v + W by Def12;
hence  v1 - v2 in W by A1, Th84; ::_thesis: verum
end;
assume  v1 - v2 in W ; ::_thesis: ex C being Coset of W st
( v1 in C & v2 in C )
then consider v being VECTOR of V such that
A2: ( v1 in v + W & v2 in v + W ) by Th84;
reconsider C = v + W as Coset of W by Def12;
take  C ; ::_thesis: ( v1 in C & v2 in C )
thus  ( v1 in C & v2 in C ) by A2; ::_thesis: verum
end;

theorem :: CLVECT_1:101
for V being ComplexLinearSpace
for u being VECTOR of V
for W being Subspace of V
for B, C being Coset of W st u in B & u in C holds
B = C
proof
let V be ComplexLinearSpace; ::_thesis: for u being VECTOR of V
for W being Subspace of V
for B, C being Coset of W st u in B & u in C holds
B = C
let u be VECTOR of V; ::_thesis: for W being Subspace of V
for B, C being Coset of W st u in B & u in C holds
B = C
let W be Subspace of V; ::_thesis: for B, C being Coset of W st u in B & u in C holds
B = C
let B, C be Coset of W; ::_thesis: ( u in B & u in C implies B = C )
assume A1: ( u in B & u in C ) ; ::_thesis: B = C
 ( ex v1 being VECTOR of V st B = v1 + W & ex v2 being VECTOR of V st C = v2 + W ) by Def12;
hence  B = C by A1, Th75; ::_thesis: verum
end;

begin

definition
attrc1 is strict ;
struct CNORMSTR  ->  CLSStruct , N-ZeroStr ;
aggrCNORMSTR(# carrier, ZeroF, addF, Mult, normF #) ->  CNORMSTR ;
end;

registration
cluster non empty for CNORMSTR ;
existence
 not for b1 being CNORMSTR holds b1 is empty
proof
set A = the non empty set ;
set Z = the Element of the non empty set ;
set a = the BinOp of the non empty set ;
set M = the Function of [:COMPLEX, the non empty set :], the non empty set ;
set n = the Function of the non empty set ,REAL;
take  CNORMSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of the non empty set ,REAL #) ; ::_thesis: not CNORMSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of the non empty set ,REAL #) is empty
thus  not the carrier of CNORMSTR(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Function of the non empty set ,REAL #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

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)
proof
let u be VECTOR of ((0). the ComplexLinearSpace); ::_thesis: for z being Complex holds niltonil . (z * u) = |.z.| * (niltonil . u)
let z be Complex; ::_thesis: niltonil . (z * u) = |.z.| * (niltonil . u)
 niltonil . u = 0 by FUNCOP_1:7;
hence  niltonil . (z * u) = |.z.| * (niltonil . u) by FUNCOP_1:7; ::_thesis: verum
end;

Lm10:  for u, v being VECTOR of ((0). the ComplexLinearSpace) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
proof
let u, v be VECTOR of ((0). the ComplexLinearSpace); ::_thesis: niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
 ( u = 0. the ComplexLinearSpace & v = 0. the ComplexLinearSpace ) by Lm7, TARSKI:def_1;
hence  niltonil . (u + v) <= (niltonil . u) + (niltonil . v) by Lm7, Lm8, TARSKI:def_1; ::_thesis: verum
end;

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 ;

Lm11: now__::_thesis:_for_x,_y_being_Point_of_X
for_z_being_Complex_holds_
(_(_||.x.||_=_0_implies_x_=_H1(X)_)_&_(_x_=_H1(X)_implies_||.x.||_=_0_)_&_||.(z_*_x).||_=_|.z.|_*_||.x.||_&_||.(x_+_y).||_<=_||.x.||_+_||.y.||_)
let x, y be Point of X; ::_thesis: for z being Complex holds
( ( ||.x.|| = 0 implies x = H1(X) ) & ( x = H1(X) implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let z be Complex; ::_thesis: ( ( ||.x.|| = 0 implies x = H1(X) ) & ( x = H1(X) implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
reconsider u = x, w = y as VECTOR of ((0). the ComplexLinearSpace) ;
 H1(X) = 0. the ComplexLinearSpace by Def8;
hence  ( ||.x.|| = 0 iff x = H1(X) ) by Lm7, FUNCOP_1:7, TARSKI:def_1; ::_thesis: ( ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
 z * x = z * u ;
hence  ||.(z * x).|| = |.z.| * ||.x.|| by Lm9; ::_thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
 x + y = u + w ;
hence  ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm10; ::_thesis: verum
end;

definition
let IT be non empty CNORMSTR ;
attrIT is ComplexNormSpace-like  means :Def13: :: CLVECT_1:def 13
 for x, y being Point of IT
for z being Complex holds
( ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| );
end;

:: deftheorem Def13 defines ComplexNormSpace-like CLVECT_1:def_13_:_
 for IT being non empty CNORMSTR holds
( IT is ComplexNormSpace-like iff for x, y being Point of IT
for z being Complex holds
( ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );

registration
cluster non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital strict ComplexNormSpace-like for CNORMSTR ;
existence
 ex b1 being non empty CNORMSTR st
( b1 is reflexive & b1 is discerning & b1 is ComplexNormSpace-like & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof
take  X ; ::_thesis: ( X is reflexive & X is discerning & X is ComplexNormSpace-like & X is vector-distributive & X is scalar-distributive & X is scalar-associative & X is scalar-unital & X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
thus  X is reflexive ::_thesis: ( X is discerning & X is ComplexNormSpace-like & X is vector-distributive & X is scalar-distributive & X is scalar-associative & X is scalar-unital & X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
proof
thus  ||.(0. X).|| = 0 by Lm11; :: according to NORMSP_0:def_6 ::_thesis: verum
end;
thus  ( X is discerning & X is ComplexNormSpace-like ) by Def13, Lm11, NORMSP_0:def_5; ::_thesis: ( X is vector-distributive & X is scalar-distributive & X is scalar-associative & X is scalar-unital & X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
thus  ( X is vector-distributive & X is scalar-distributive & X is scalar-associative & X is scalar-unital ) ::_thesis: ( X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
proof
thus  for z being Complex
for v, w being VECTOR of X holds z * (v + w) = (z * v) + (z * w) :: according to CLVECT_1:def_2 ::_thesis: ( X is scalar-distributive & X is scalar-associative & X is scalar-unital )
proof
let z be Complex; ::_thesis: for v, w being VECTOR of X holds z * (v + w) = (z * v) + (z * w)
let v, w be VECTOR of X; ::_thesis: z * (v + w) = (z * v) + (z * w)
reconsider v9 = v, w9 = w as VECTOR of ((0). the ComplexLinearSpace) ;
thus z * (v + w) = z * (v9 + w9)
.= (z * v9) + (z * w9) by Def2
.= (z * v) + (z * w) ; ::_thesis: verum
end;
thus  for z1, z2 being Complex
for v being VECTOR of X holds (z1 + z2) * v = (z1 * v) + (z2 * v) :: according to CLVECT_1:def_3 ::_thesis: ( X is scalar-associative & X is scalar-unital )
proof
let z1, z2 be Complex; ::_thesis: for v being VECTOR of X holds (z1 + z2) * v = (z1 * v) + (z2 * v)
let v be VECTOR of X; ::_thesis: (z1 + z2) * v = (z1 * v) + (z2 * v)
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
thus (z1 + z2) * v = (z1 + z2) * v9
.= (z1 * v9) + (z2 * v9) by Def3
.= (z1 * v) + (z2 * v) ; ::_thesis: verum
end;
thus  for z1, z2 being Complex
for v being VECTOR of X holds (z1 * z2) * v = z1 * (z2 * v) :: according to CLVECT_1:def_4 ::_thesis: X is scalar-unital
proof
let z1, z2 be Complex; ::_thesis: for v being VECTOR of X holds (z1 * z2) * v = z1 * (z2 * v)
let v be VECTOR of X; ::_thesis: (z1 * z2) * v = z1 * (z2 * v)
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
thus (z1 * z2) * v = (z1 * z2) * v9
.= z1 * (z2 * v9) by Def4
.= z1 * (z2 * v) ; ::_thesis: verum
end;
let v be VECTOR of X; :: according to CLVECT_1:def_5 ::_thesis: 1r * v = v
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
thus 1r * v = 1r * v9
.= v by Def5 ; ::_thesis: verum
end;
A1: for x, y being VECTOR of X
for x9, y9 being VECTOR of ((0). the ComplexLinearSpace) st x = x9 & y = y9 holds
( x + y = x9 + y9 & ( for z being Complex holds z * x = z * x9 ) ) ;
thus  for v, w being VECTOR of X holds v + w = w + v :: according to RLVECT_1:def_2 ::_thesis: ( X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
proof
let v, w be VECTOR of X; ::_thesis: v + w = w + v
reconsider v9 = v, w9 = w as VECTOR of ((0). the ComplexLinearSpace) ;
thus v + w = w9 + v9 by A1
.= w + v ; ::_thesis: verum
end;
thus  for u, v, w being VECTOR of X holds (u + v) + w = u + (v + w) :: according to RLVECT_1:def_3 ::_thesis: ( X is right_zeroed & X is right_complementable & X is strict )
proof
let u, v, w be VECTOR of X; ::_thesis: (u + v) + w = u + (v + w)
reconsider u9 = u, v9 = v, w9 = w as VECTOR of ((0). the ComplexLinearSpace) ;
thus (u + v) + w = (u9 + v9) + w9
.= u9 + (v9 + w9) by RLVECT_1:def_3
.= u + (v + w) ; ::_thesis: verum
end;
thus  for v being VECTOR of X holds v + (0. X) = v :: according to RLVECT_1:def_4 ::_thesis: ( X is right_complementable & X is strict )
proof
let v be VECTOR of X; ::_thesis: v + (0. X) = v
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
thus v + (0. X) = v9 + (0. ((0). the ComplexLinearSpace))
.= v by RLVECT_1:4 ; ::_thesis: verum
end;
thus  X is right_complementable ::_thesis: X is strict
proof
let v be VECTOR of X; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
consider w9 being VECTOR of ((0). the ComplexLinearSpace) such that
A2: v9 + w9 = 0. ((0). the ComplexLinearSpace) by ALGSTR_0:def_11;
reconsider w = w9 as VECTOR of X ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. X
thus  v + w = 0. X by A2; ::_thesis: verum
end;
thus  X is strict ; ::_thesis: verum
end;
end;

definition
mode ComplexNormSpace is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR ;
end;


theorem :: CLVECT_1:102
for CNS being ComplexNormSpace holds ||.(0. CNS).|| = 0 ;

theorem Th103: :: CLVECT_1:103
for CNS being ComplexNormSpace
for x being Point of CNS holds ||.(- x).|| = ||.x.||
proof
let CNS be ComplexNormSpace; ::_thesis: for x being Point of CNS holds ||.(- x).|| = ||.x.||
let x be Point of CNS; ::_thesis: ||.(- x).|| = ||.x.||
A1: |.(- 1r).| = 1 by COMPLEX1:48, COMPLEX1:52;
||.(- x).|| = ||.((- 1r) * x).|| by Th3
.= |.(- 1r).| * ||.x.|| by Def13 ;
hence  ||.(- x).|| = ||.x.|| by A1; ::_thesis: verum
end;

theorem Th104: :: CLVECT_1:104
for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.(x - y).|| <= ||.x.|| + ||.y.||
proof
let CNS be ComplexNormSpace; ::_thesis: for x, y being Point of CNS holds ||.(x - y).|| <= ||.x.|| + ||.y.||
let x, y be Point of CNS; ::_thesis: ||.(x - y).|| <= ||.x.|| + ||.y.||
 ||.(x - y).|| <= ||.x.|| + ||.(- y).|| by Def13;
hence  ||.(x - y).|| <= ||.x.|| + ||.y.|| by Th103; ::_thesis: verum
end;

theorem Th105: :: CLVECT_1:105
for CNS being ComplexNormSpace
for x being Point of CNS holds 0 <= ||.x.||
proof
let CNS be ComplexNormSpace; ::_thesis: for x being Point of CNS holds 0 <= ||.x.||
let x be Point of CNS; ::_thesis: 0 <= ||.x.||
||.(x - x).|| = ||.H1(CNS).|| by RLVECT_1:15
.= 0 ;
then  0 <= (||.x.|| + ||.x.||) / 2 by Th104;
hence  0 <= ||.x.|| ; ::_thesis: verum
end;

theorem :: CLVECT_1:106
for z1, z2 being Complex
for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)
proof
let z1, z2 be Complex; ::_thesis: for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)
let CNS be ComplexNormSpace; ::_thesis: for x, y being Point of CNS holds ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)
let x, y be Point of CNS; ::_thesis: ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)
 ||.((z1 * x) + (z2 * y)).|| <= ||.(z1 * x).|| + ||.(z2 * y).|| by Def13;
then  ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + ||.(z2 * y).|| by Def13;
hence  ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||) by Def13; ::_thesis: verum
end;

theorem Th107: :: CLVECT_1:107
for CNS being ComplexNormSpace
for x, y being Point of CNS holds
( ||.(x - y).|| = 0 iff x = y )
proof
let CNS be ComplexNormSpace; ::_thesis: for x, y being Point of CNS holds
( ||.(x - y).|| = 0 iff x = y )
let x, y be Point of CNS; ::_thesis: ( ||.(x - y).|| = 0 iff x = y )
 ( ||.(x - y).|| = 0 iff x - y = H1(CNS) ) by NORMSP_0:def_5;
hence  ( ||.(x - y).|| = 0 iff x = y ) by RLVECT_1:15, RLVECT_1:21; ::_thesis: verum
end;

theorem Th108: :: CLVECT_1:108
for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.(x - y).|| = ||.(y - x).||
proof
let CNS be ComplexNormSpace; ::_thesis: for x, y being Point of CNS holds ||.(x - y).|| = ||.(y - x).||
let x, y be Point of CNS; ::_thesis: ||.(x - y).|| = ||.(y - x).||
 x - y = - (y - x) by RLVECT_1:33;
hence  ||.(x - y).|| = ||.(y - x).|| by Th103; ::_thesis: verum
end;

theorem Th109: :: CLVECT_1:109
for CNS being ComplexNormSpace
for x, y being Point of CNS holds ||.x.|| - ||.y.|| <= ||.(x - y).||
proof
let CNS be ComplexNormSpace; ::_thesis: for x, y being Point of CNS holds ||.x.|| - ||.y.|| <= ||.(x - y).||
let x, y be Point of CNS; ::_thesis: ||.x.|| - ||.y.|| <= ||.(x - y).||
(x - y) + y = x - (y - y) by RLVECT_1:29
.= x - H1(CNS) by RLVECT_1:15
.= x by RLVECT_1:13 ;
then  ||.x.|| <= ||.(x - y).|| + ||.y.|| by Def13;
hence  ||.x.|| - ||.y.|| <= ||.(x - y).|| by XREAL_1:20; ::_thesis: verum
end;

theorem Th110: :: CLVECT_1:110
for CNS being ComplexNormSpace
for x, y being Point of CNS holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
proof
let CNS be ComplexNormSpace; ::_thesis: for x, y being Point of CNS holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
let x, y be Point of CNS; ::_thesis: abs (||.x.|| - ||.y.||) <= ||.(x - y).||
(y - x) + x = y - (x - x) by RLVECT_1:29
.= y - H1(CNS) by RLVECT_1:15
.= y by RLVECT_1:13 ;
then  ||.y.|| <= ||.(y - x).|| + ||.x.|| by Def13;
then  ||.y.|| - ||.x.|| <= ||.(y - x).|| by XREAL_1:20;
then  ||.y.|| - ||.x.|| <= ||.(x - y).|| by Th108;
then A1: - ||.(x - y).|| <= - (||.y.|| - ||.x.||) by XREAL_1:24;
 ||.x.|| - ||.y.|| <= ||.(x - y).|| by Th109;
hence  abs (||.x.|| - ||.y.||) <= ||.(x - y).|| by A1, ABSVALUE:5; ::_thesis: verum
end;

theorem Th111: :: CLVECT_1:111
for CNS being ComplexNormSpace
for x, w, y being Point of CNS holds ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||
proof
let CNS be ComplexNormSpace; ::_thesis: for x, w, y being Point of CNS holds ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||
let x, w, y be Point of CNS; ::_thesis: ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||
x - w = x + (H1(CNS) + (- w)) by RLVECT_1:4
.= x + (((- y) + y) + (- w)) by RLVECT_1:5
.= x + ((- y) + (y + (- w))) by RLVECT_1:def_3
.= (x - y) + (y - w) by RLVECT_1:def_3 ;
hence  ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).|| by Def13; ::_thesis: verum
end;

theorem :: CLVECT_1:112
for CNS being ComplexNormSpace
for x, y being Point of CNS st x <> y holds
||.(x - y).|| <> 0 by Th107;


definition
let CNS be ComplexLinearSpace;
let S be sequence of CNS;
let z be Complex;
funcz * S ->  sequence of CNS means :Def14: :: CLVECT_1:def 14
 for n being Element of NAT holds it . n = z * (S . n);
existence
 ex b1 being sequence of CNS st
for n being Element of NAT holds b1 . n = z * (S . n)
proof
deffunc H2( Element of NAT ) ->  Element of CNS = z * (S . $1);
thus  ex S being sequence of CNS st
for n being Element of NAT holds S . n = H2(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of CNS st ( for n being Element of NAT holds b1 . n = z * (S . n) ) & ( for n being Element of NAT holds b2 . n = z * (S . n) ) holds
b1 = b2
proof
let S1, S2 be sequence of CNS; ::_thesis: ( ( for n being Element of NAT holds S1 . n = z * (S . n) ) & ( for n being Element of NAT holds S2 . n = z * (S . n) ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = z * (S . n) and
A2: for n being Element of NAT holds S2 . n = z * (S . n) ; ::_thesis: S1 = S2
 for n being Element of NAT holds S1 . n = S2 . n
proof
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
 S1 . n = z * (S . n) by A1;
hence  S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence  S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines * CLVECT_1:def_14_:_
 for CNS being ComplexLinearSpace
for S being sequence of CNS
for z being Complex
for b4 being sequence of CNS holds
( b4 = z * S iff for n being Element of NAT holds b4 . n = z * (S . n) );

definition
let CNS be ComplexNormSpace;
let S be sequence of CNS;
attrS is convergent  means :Def15: :: CLVECT_1:def 15
 ex g being Point of CNS st
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r;
end;

:: deftheorem Def15 defines convergent CLVECT_1:def_15_:_
 for CNS being ComplexNormSpace
for S being sequence of CNS holds
( S is convergent iff ex g being Point of CNS st
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r );

theorem Th113: :: CLVECT_1:113
for CNS being ComplexNormSpace
for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
S1 + S2 is convergent
proof
let CNS be ComplexNormSpace; ::_thesis: for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
S1 + S2 is convergent
let S1, S2 be sequence of CNS; ::_thesis: ( S1 is convergent & S2 is convergent implies S1 + S2 is convergent )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; ::_thesis: S1 + S2 is convergent
consider g1 being Point of CNS such that
A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S1 . n) - g1).|| < r by A1, Def15;
consider g2 being Point of CNS such that
A4: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S2 . n) - g2).|| < r by A2, Def15;
take g = g1 + g2; :: according to CLVECT_1:def_15 ::_thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 + S2) . n) - g).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 + S2) . n) - g).|| < r )
assume A5: 0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 + S2) . n) - g).|| < r
then consider m1 being Element of NAT  such that
A6: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - g1).|| < r / 2 by A3;
consider m2 being Element of NAT  such that
A7: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - g2).|| < r / 2 by A4, A5;
take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S1 + S2) . n) - g).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S1 + S2) . n) - g).|| < r )
assume A8: k <= n ; ::_thesis: ||.(((S1 + S2) . n) - g).|| < r
 m2 <= k by NAT_1:12;
then  m2 <= n by A8, XXREAL_0:2;
then A9: ||.((S2 . n) - g2).|| < r / 2 by A7;
A10: ||.(((S1 + S2) . n) - g).|| = ||.((- (g1 + g2)) + ((S1 . n) + (S2 . n))).|| by NORMSP_1:def_2
.= ||.(((- g1) + (- g2)) + ((S1 . n) + (S2 . n))).|| by RLVECT_1:31
.= ||.(((S1 . n) + ((- g1) + (- g2))) + (S2 . n)).|| by RLVECT_1:def_3
.= ||.((((S1 . n) - g1) + (- g2)) + (S2 . n)).|| by RLVECT_1:def_3
.= ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| by RLVECT_1:def_3 ;
A11: ||.(((S1 . n) - g1) + ((S2 . n) - g2)).|| <= ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| by Def13;
 m1 <= m1 + m2 by NAT_1:12;
then  m1 <= n by A8, XXREAL_0:2;
then  ||.((S1 . n) - g1).|| < r / 2 by A6;
then  ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| < (r / 2) + (r / 2) by A9, XREAL_1:8;
hence  ||.(((S1 + S2) . n) - g).|| < r by A10, A11, XXREAL_0:2; ::_thesis: verum
end;

theorem Th114: :: CLVECT_1:114
for CNS being ComplexNormSpace
for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
S1 - S2 is convergent
proof
let CNS be ComplexNormSpace; ::_thesis: for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
S1 - S2 is convergent
let S1, S2 be sequence of CNS; ::_thesis: ( S1 is convergent & S2 is convergent implies S1 - S2 is convergent )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; ::_thesis: S1 - S2 is convergent
consider g1 being Point of CNS such that
A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S1 . n) - g1).|| < r by A1, Def15;
consider g2 being Point of CNS such that
A4: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S2 . n) - g2).|| < r by A2, Def15;
take g = g1 - g2; :: according to CLVECT_1:def_15 ::_thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 - S2) . n) - g).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 - S2) . n) - g).|| < r )
assume A5: 0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S1 - S2) . n) - g).|| < r
then consider m1 being Element of NAT  such that
A6: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - g1).|| < r / 2 by A3;
consider m2 being Element of NAT  such that
A7: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - g2).|| < r / 2 by A4, A5;
take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - g).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S1 - S2) . n) - g).|| < r )
assume A8: k <= n ; ::_thesis: ||.(((S1 - S2) . n) - g).|| < r
 m2 <= k by NAT_1:12;
then  m2 <= n by A8, XXREAL_0:2;
then A9: ||.((S2 . n) - g2).|| < r / 2 by A7;
A10: ||.(((S1 - S2) . n) - g).|| = ||.(((S1 . n) - (S2 . n)) - (g1 - g2)).|| by NORMSP_1:def_3
.= ||.((((S1 . n) - (S2 . n)) - g1) + g2).|| by RLVECT_1:29
.= ||.(((S1 . n) - (g1 + (S2 . n))) + g2).|| by RLVECT_1:27
.= ||.((((S1 . n) - g1) - (S2 . n)) + g2).|| by RLVECT_1:27
.= ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| by RLVECT_1:29 ;
A11: ||.(((S1 . n) - g1) - ((S2 . n) - g2)).|| <= ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| by Th104;
 m1 <= m1 + m2 by NAT_1:12;
then  m1 <= n by A8, XXREAL_0:2;
then  ||.((S1 . n) - g1).|| < r / 2 by A6;
then  ||.((S1 . n) - g1).|| + ||.((S2 . n) - g2).|| < (r / 2) + (r / 2) by A9, XREAL_1:8;
hence  ||.(((S1 - S2) . n) - g).|| < r by A10, A11, XXREAL_0:2; ::_thesis: verum
end;

theorem Th115: :: CLVECT_1:115
for CNS being ComplexNormSpace
for x being Point of CNS
for S being sequence of CNS st S is convergent holds
S - x is convergent
proof
let CNS be ComplexNormSpace; ::_thesis: for x being Point of CNS
for S being sequence of CNS st S is convergent holds
S - x is convergent
let x be Point of CNS; ::_thesis: for S being sequence of CNS st S is convergent holds
S - x is convergent
let S be sequence of CNS; ::_thesis: ( S is convergent implies S - x is convergent )
assume  S is convergent ; ::_thesis: S - x is convergent
then consider g being Point of CNS such that
A1: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r by Def15;
take h = g - x; :: according to CLVECT_1:def_15 ::_thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S - x) . n) - h).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S - x) . n) - h).|| < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((S - x) . n) - h).|| < r
then consider m1 being Element of NAT  such that
A2: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S - x) . n) - h).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S - x) . n) - h).|| < r )
assume  k <= n ; ::_thesis: ||.(((S - x) . n) - h).|| < r
then A3: ||.((S . n) - g).|| < r by A2;
||.((S . n) - g).|| = ||.(((S . n) - H1(CNS)) - g).|| by RLVECT_1:13
.= ||.(((S . n) - (x - x)) - g).|| by RLVECT_1:15
.= ||.((((S . n) - x) + x) - g).|| by RLVECT_1:29
.= ||.(((S . n) - x) + ((- g) + x)).|| by RLVECT_1:def_3
.= ||.(((S . n) - x) - h).|| by RLVECT_1:33 ;
hence  ||.(((S - x) . n) - h).|| < r by A3, NORMSP_1:def_4; ::_thesis: verum
end;

theorem Th116: :: CLVECT_1:116
for z being Complex
for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
z * S is convergent
proof
let z be Complex; ::_thesis: for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
z * S is convergent
let CNS be ComplexNormSpace; ::_thesis: for S being sequence of CNS st S is convergent holds
z * S is convergent
let S be sequence of CNS; ::_thesis: ( S is convergent implies z * S is convergent )
assume  S is convergent ; ::_thesis: z * S is convergent
then consider g being Point of CNS such that
A1: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r by Def15;
take h = z * g; :: according to CLVECT_1:def_15 ::_thesis: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((z * S) . n) - h).|| < r
A2: now__::_thesis:_(_z_<>_0c_implies_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((z_*_S)_._n)_-_h).||_<_r_)
assume A3: z <> 0c ; ::_thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r
then A4: 0 < |.z.| by COMPLEX1:47;
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r / |.z.| by A1, A4;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((z * S) . n) - h).|| < r )
assume  k <= n ; ::_thesis: ||.(((z * S) . n) - h).|| < r
then A6: ||.((S . n) - g).|| < r / |.z.| by A5;
A7: 0 <> |.z.| by A3, COMPLEX1:47;
A8: |.z.| * (r / |.z.|) = |.z.| * ((|.z.| ") * r) by XCMPLX_0:def_9
.= (|.z.| * (|.z.| ")) * r
.= 1 * r by A7, XCMPLX_0:def_7
.= r ;
||.((z * (S . n)) - (z * g)).|| = ||.(z * ((S . n) - g)).|| by Th9
.= |.z.| * ||.((S . n) - g).|| by Def13 ;
then  ||.((z * (S . n)) - h).|| < r by A4, A6, A8, XREAL_1:68;
hence  ||.(((z * S) . n) - h).|| < r by Def14; ::_thesis: verum
end;
now__::_thesis:_(_z_=_0_implies_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((z_*_S)_._n)_-_h).||_<_r_)
assume A9: z = 0 ; ::_thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r
then consider m1 being Element of NAT  such that
A10: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((z * S) . n) - h).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((z * S) . n) - h).|| < r )
assume  k <= n ; ::_thesis: ||.(((z * S) . n) - h).|| < r
then A11: ||.((S . n) - g).|| < r by A10;
||.((z * (S . n)) - (z * g)).|| = ||.((0c * (S . n)) - H1(CNS)).|| by A9, Th1
.= ||.(H1(CNS) - H1(CNS)).|| by Th1
.= ||.H1(CNS).|| by RLVECT_1:13
.= 0 ;
then  ||.((z * (S . n)) - h).|| < r by A11, Th105;
hence  ||.(((z * S) . n) - h).|| < r by Def14; ::_thesis: verum
end;
hence  for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((z * S) . n) - h).|| < r by A2; ::_thesis: verum
end;

theorem Th117: :: CLVECT_1:117
for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
||.S.|| is convergent
proof
let CNS be ComplexNormSpace; ::_thesis: for S being sequence of CNS st S is convergent holds
||.S.|| is convergent
let S be sequence of CNS; ::_thesis: ( S is convergent implies ||.S.|| is convergent )
assume  S is convergent ; ::_thesis: ||.S.|| is convergent
then consider g being Point of CNS such that
A1: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r by Def15;
now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
abs_((||.S.||_._n)_-_||.g.||)_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.S.|| . n) - ||.g.||) < r )
assume A2: 0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.S.|| . n) - ||.g.||) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A3: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1, A2;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
abs ((||.S.|| . n) - ||.g.||) < r
let n be Element of NAT ; ::_thesis: ( k <= n implies abs ((||.S.|| . n) - ||.g.||) < r )
assume  k <= n ; ::_thesis: abs ((||.S.|| . n) - ||.g.||) < r
then A4: ||.((S . n) - g).|| < r by A3;
 abs (||.(S . n).|| - ||.g.||) <= ||.((S . n) - g).|| by Th110;
then  abs (||.(S . n).|| - ||.g.||) < r by A4, XXREAL_0:2;
hence  abs ((||.S.|| . n) - ||.g.||) < r by NORMSP_0:def_4; ::_thesis: verum
end;
hence  ||.S.|| is convergent by SEQ_2:def_6; ::_thesis: verum
end;

definition
let CNS be ComplexNormSpace;
let S be sequence of CNS;
assume A1: S is convergent ;
func lim S ->  Point of CNS means :Def16: :: CLVECT_1:def 16
 for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - it).|| < r;
existence
 ex b1 being Point of CNS st
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b1).|| < r by A1, Def15;
uniqueness
 for b1, b2 being Point of CNS st ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b1).|| < r ) & ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b2).|| < r ) holds
b1 = b2
proof
 for x, y being Point of CNS st ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r ) & ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - y).|| < r ) holds
x = y
proof
given x, y being Point of CNS such that A2: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - x).|| < r and
A3: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - y).|| < r and
A4: x <> y ; ::_thesis: contradiction
A5: 0 <= ||.(x - y).|| by Th105;
A6: ||.(x - y).|| <> 0 by A4, Th107;
then consider m1 being Element of NAT  such that
A7: for n being Element of NAT st m1 <= n holds
||.((S . n) - x).|| < ||.(x - y).|| / 4 by A2, A5;
consider m2 being Element of NAT  such that
A8: for n being Element of NAT st m2 <= n holds
||.((S . n) - y).|| < ||.(x - y).|| / 4 by A3, A6, A5;
A9: now__::_thesis:_not_m2_<=_m1
 ||.(x - y).|| <= ||.(x - (S . m1)).|| + ||.((S . m1) - y).|| by Th111;
then A10: ||.(x - y).|| <= ||.((S . m1) - x).|| + ||.((S . m1) - y).|| by Th108;
assume  m2 <= m1 ; ::_thesis: contradiction
then A11: ||.((S . m1) - y).|| < ||.(x - y).|| / 4 by A8;
 ||.((S . m1) - x).|| < ||.(x - y).|| / 4 by A7;
then  ||.((S . m1) - x).|| + ||.((S . m1) - y).|| < (||.(x - y).|| / 4) + (||.(x - y).|| / 4) by A11, XREAL_1:8;
then  not ||.(x - y).|| / 2 < ||.(x - y).|| by A10, XXREAL_0:2;
hence  contradiction by A6, A5, XREAL_1:216; ::_thesis: verum
end;
now__::_thesis:_not_m1_<=_m2
 ||.(x - y).|| <= ||.(x - (S . m2)).|| + ||.((S . m2) - y).|| by Th111;
then A12: ||.(x - y).|| <= ||.((S . m2) - x).|| + ||.((S . m2) - y).|| by Th108;
assume  m1 <= m2 ; ::_thesis: contradiction
then A13: ||.((S . m2) - x).|| < ||.(x - y).|| / 4 by A7;
 ||.((S . m2) - y).|| < ||.(x - y).|| / 4 by A8;
then  ||.((S . m2) - x).|| + ||.((S . m2) - y).|| < (||.(x - y).|| / 4) + (||.(x - y).|| / 4) by A13, XREAL_1:8;
then  not ||.(x - y).|| / 2 < ||.(x - y).|| by A12, XXREAL_0:2;
hence  contradiction by A6, A5, XREAL_1:216; ::_thesis: verum
end;
hence  contradiction by A9; ::_thesis: verum
end;
hence  for b1, b2 being Point of CNS st ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b1).|| < r ) & ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b2).|| < r ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines lim CLVECT_1:def_16_:_
 for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
for b3 being Point of CNS holds
( b3 = lim S iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b3).|| < r );

theorem :: CLVECT_1:118
for CNS being ComplexNormSpace
for g being Point of CNS
for S being sequence of CNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
proof
let CNS be ComplexNormSpace; ::_thesis: for g being Point of CNS
for S being sequence of CNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
let g be Point of CNS; ::_thesis: for S being sequence of CNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
let S be sequence of CNS; ::_thesis: ( S is convergent & lim S = g implies ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )
assume that
A1: S is convergent and
A2: lim S = g ; ::_thesis: ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
A3: now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
abs_((||.(S_-_g).||_._n)_-_0)_<_r
let r be real number ; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.(S - g).|| . n) - 0) < r )
assume A4: 0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.(S - g).|| . n) - 0) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1, A2, A4, Def16;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
abs ((||.(S - g).|| . n) - 0) < r
let n be Element of NAT ; ::_thesis: ( k <= n implies abs ((||.(S - g).|| . n) - 0) < r )
assume  k <= n ; ::_thesis: abs ((||.(S - g).|| . n) - 0) < r
then  ||.((S . n) - g).|| < r by A5;
then A6: ||.(((S . n) - g) - H1(CNS)).|| < r by RLVECT_1:13;
 abs (||.((S . n) - g).|| - ||.H1(CNS).||) <= ||.(((S . n) - g) - H1(CNS)).|| by Th110;
then  abs (||.((S . n) - g).|| - ||.H1(CNS).||) < r by A6, XXREAL_0:2;
then  abs (||.((S . n) - g).|| - 0) < r ;
then  abs (||.((S - g) . n).|| - 0) < r by NORMSP_1:def_4;
hence  abs ((||.(S - g).|| . n) - 0) < r by NORMSP_0:def_4; ::_thesis: verum
end;
 ||.(S - g).|| is convergent by A1, Th115, Th117;
hence  ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) by A3, SEQ_2:def_7; ::_thesis: verum
end;

theorem :: CLVECT_1:119
for CNS being ComplexNormSpace
for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
lim (S1 + S2) = (lim S1) + (lim S2)
proof
let CNS be ComplexNormSpace; ::_thesis: for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
lim (S1 + S2) = (lim S1) + (lim S2)
let S1, S2 be sequence of CNS; ::_thesis: ( S1 is convergent & S2 is convergent implies lim (S1 + S2) = (lim S1) + (lim S2) )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; ::_thesis: lim (S1 + S2) = (lim S1) + (lim S2)
set g2 = lim S2;
set g1 = lim S1;
set g = (lim S1) + (lim S2);
A3: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((S1_+_S2)_._n)_-_((lim_S1)_+_(lim_S2))).||_<_r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r )
assume A4: 0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - (lim S1)).|| < r / 2 by A1, Def16;
consider m2 being Element of NAT  such that
A6: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - (lim S2)).|| < r / 2 by A2, A4, Def16;
take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r )
assume A7: k <= n ; ::_thesis: ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r
 m2 <= k by NAT_1:12;
then  m2 <= n by A7, XXREAL_0:2;
then A8: ||.((S2 . n) - (lim S2)).|| < r / 2 by A6;
A9: ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| = ||.((- ((lim S1) + (lim S2))) + ((S1 . n) + (S2 . n))).|| by NORMSP_1:def_2
.= ||.(((- (lim S1)) + (- (lim S2))) + ((S1 . n) + (S2 . n))).|| by RLVECT_1:31
.= ||.(((S1 . n) + ((- (lim S1)) + (- (lim S2)))) + (S2 . n)).|| by RLVECT_1:def_3
.= ||.((((S1 . n) - (lim S1)) + (- (lim S2))) + (S2 . n)).|| by RLVECT_1:def_3
.= ||.(((S1 . n) - (lim S1)) + ((S2 . n) - (lim S2))).|| by RLVECT_1:def_3 ;
A10: ||.(((S1 . n) - (lim S1)) + ((S2 . n) - (lim S2))).|| <= ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| by Def13;
 m1 <= m1 + m2 by NAT_1:12;
then  m1 <= n by A7, XXREAL_0:2;
then  ||.((S1 . n) - (lim S1)).|| < r / 2 by A5;
then  ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence  ||.(((S1 + S2) . n) - ((lim S1) + (lim S2))).|| < r by A9, A10, XXREAL_0:2; ::_thesis: verum
end;
 S1 + S2 is convergent by A1, A2, Th113;
hence  lim (S1 + S2) = (lim S1) + (lim S2) by A3, Def16; ::_thesis: verum
end;

theorem :: CLVECT_1:120
for CNS being ComplexNormSpace
for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
lim (S1 - S2) = (lim S1) - (lim S2)
proof
let CNS be ComplexNormSpace; ::_thesis: for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds
lim (S1 - S2) = (lim S1) - (lim S2)
let S1, S2 be sequence of CNS; ::_thesis: ( S1 is convergent & S2 is convergent implies lim (S1 - S2) = (lim S1) - (lim S2) )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; ::_thesis: lim (S1 - S2) = (lim S1) - (lim S2)
set g2 = lim S2;
set g1 = lim S1;
set g = (lim S1) - (lim S2);
A3: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((S1_-_S2)_._n)_-_((lim_S1)_-_(lim_S2))).||_<_r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r )
assume A4: 0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - (lim S1)).|| < r / 2 by A1, Def16;
consider m2 being Element of NAT  such that
A6: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - (lim S2)).|| < r / 2 by A2, A4, Def16;
take k = m1 + m2; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r )
assume A7: k <= n ; ::_thesis: ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
 m2 <= k by NAT_1:12;
then  m2 <= n by A7, XXREAL_0:2;
then A8: ||.((S2 . n) - (lim S2)).|| < r / 2 by A6;
A9: ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| = ||.(((S1 . n) - (S2 . n)) - ((lim S1) - (lim S2))).|| by NORMSP_1:def_3
.= ||.((((S1 . n) - (S2 . n)) - (lim S1)) + (lim S2)).|| by RLVECT_1:29
.= ||.(((S1 . n) - ((lim S1) + (S2 . n))) + (lim S2)).|| by RLVECT_1:27
.= ||.((((S1 . n) - (lim S1)) - (S2 . n)) + (lim S2)).|| by RLVECT_1:27
.= ||.(((S1 . n) - (lim S1)) - ((S2 . n) - (lim S2))).|| by RLVECT_1:29 ;
A10: ||.(((S1 . n) - (lim S1)) - ((S2 . n) - (lim S2))).|| <= ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| by Th104;
 m1 <= m1 + m2 by NAT_1:12;
then  m1 <= n by A7, XXREAL_0:2;
then  ||.((S1 . n) - (lim S1)).|| < r / 2 by A5;
then  ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence  ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r by A9, A10, XXREAL_0:2; ::_thesis: verum
end;
 S1 - S2 is convergent by A1, A2, Th114;
hence  lim (S1 - S2) = (lim S1) - (lim S2) by A3, Def16; ::_thesis: verum
end;

theorem :: CLVECT_1:121
for CNS being ComplexNormSpace
for x being Point of CNS
for S being sequence of CNS st S is convergent holds
lim (S - x) = (lim S) - x
proof
let CNS be ComplexNormSpace; ::_thesis: for x being Point of CNS
for S being sequence of CNS st S is convergent holds
lim (S - x) = (lim S) - x
let x be Point of CNS; ::_thesis: for S being sequence of CNS st S is convergent holds
lim (S - x) = (lim S) - x
let S be sequence of CNS; ::_thesis: ( S is convergent implies lim (S - x) = (lim S) - x )
set g = lim S;
set h = (lim S) - x;
assume A1: S is convergent ; ::_thesis: lim (S - x) = (lim S) - x
A2: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((S_-_x)_._n)_-_((lim_S)_-_x)).||_<_r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S - x) . n) - ((lim S) - x)).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S - x) . n) - ((lim S) - x)).|| < r
then consider m1 being Element of NAT  such that
A3: for n being Element of NAT st m1 <= n holds
||.((S . n) - (lim S)).|| < r by A1, Def16;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((S - x) . n) - ((lim S) - x)).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((S - x) . n) - ((lim S) - x)).|| < r )
assume  k <= n ; ::_thesis: ||.(((S - x) . n) - ((lim S) - x)).|| < r
then A4: ||.((S . n) - (lim S)).|| < r by A3;
||.((S . n) - (lim S)).|| = ||.(((S . n) - H1(CNS)) - (lim S)).|| by RLVECT_1:13
.= ||.(((S . n) - (x - x)) - (lim S)).|| by RLVECT_1:15
.= ||.((((S . n) - x) + x) - (lim S)).|| by RLVECT_1:29
.= ||.(((S . n) - x) + ((- (lim S)) + x)).|| by RLVECT_1:def_3
.= ||.(((S . n) - x) - ((lim S) - x)).|| by RLVECT_1:33 ;
hence  ||.(((S - x) . n) - ((lim S) - x)).|| < r by A4, NORMSP_1:def_4; ::_thesis: verum
end;
 S - x is convergent by A1, Th115;
hence  lim (S - x) = (lim S) - x by A2, Def16; ::_thesis: verum
end;

theorem :: CLVECT_1:122
for z being Complex
for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
lim (z * S) = z * (lim S)
proof
let z be Complex; ::_thesis: for CNS being ComplexNormSpace
for S being sequence of CNS st S is convergent holds
lim (z * S) = z * (lim S)
let CNS be ComplexNormSpace; ::_thesis: for S being sequence of CNS st S is convergent holds
lim (z * S) = z * (lim S)
let S be sequence of CNS; ::_thesis: ( S is convergent implies lim (z * S) = z * (lim S) )
set g = lim S;
set h = z * (lim S);
assume A1: S is convergent ; ::_thesis: lim (z * S) = z * (lim S)
A2: now__::_thesis:_(_z_=_0_implies_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((z_*_S)_._n)_-_(z_*_(lim_S))).||_<_r_)
assume A3: z = 0 ; ::_thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
then consider m1 being Element of NAT  such that
A4: for n being Element of NAT st m1 <= n holds
||.((S . n) - (lim S)).|| < r by A1, Def16;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((z * S) . n) - (z * (lim S))).|| < r )
assume  k <= n ; ::_thesis: ||.(((z * S) . n) - (z * (lim S))).|| < r
then A5: ||.((S . n) - (lim S)).|| < r by A4;
||.((z * (S . n)) - (z * (lim S))).|| = ||.((0c * (S . n)) - H1(CNS)).|| by A3, Th1
.= ||.(H1(CNS) - H1(CNS)).|| by Th1
.= ||.H1(CNS).|| by RLVECT_1:13
.= 0 ;
then  ||.((z * (S . n)) - (z * (lim S))).|| < r by A5, Th105;
hence  ||.(((z * S) . n) - (z * (lim S))).|| < r by Def14; ::_thesis: verum
end;
A6: now__::_thesis:_(_z_<>_0c_implies_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
||.(((z_*_S)_._n)_-_(z_*_(lim_S))).||_<_r_)
assume A7: z <> 0c ; ::_thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
then A8: 0 < |.z.| by COMPLEX1:47;
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
then consider m1 being Element of NAT  such that
A9: for n being Element of NAT st m1 <= n holds
||.((S . n) - (lim S)).|| < r / |.z.| by A1, A8, Def16;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
||.(((z * S) . n) - (z * (lim S))).|| < r
let n be Element of NAT ; ::_thesis: ( k <= n implies ||.(((z * S) . n) - (z * (lim S))).|| < r )
assume  k <= n ; ::_thesis: ||.(((z * S) . n) - (z * (lim S))).|| < r
then A10: ||.((S . n) - (lim S)).|| < r / |.z.| by A9;
A11: 0 <> |.z.| by A7, COMPLEX1:47;
A12: |.z.| * (r / |.z.|) = |.z.| * ((|.z.| ") * r) by XCMPLX_0:def_9
.= (|.z.| * (|.z.| ")) * r
.= 1 * r by A11, XCMPLX_0:def_7
.= r ;
||.((z * (S . n)) - (z * (lim S))).|| = ||.(z * ((S . n) - (lim S))).|| by Th9
.= |.z.| * ||.((S . n) - (lim S)).|| by Def13 ;
then  ||.((z * (S . n)) - (z * (lim S))).|| < r by A8, A10, A12, XREAL_1:68;
hence  ||.(((z * S) . n) - (z * (lim S))).|| < r by Def14; ::_thesis: verum
end;
 z * S is convergent by A1, Th116;
hence  lim (z * S) = z * (lim S) by A2, A6, Def16; ::_thesis: verum
end;

theorem :: CLVECT_1:123
for z being Complex
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 V being ComplexLinearSpace
for V1 being Subset of V
for v being VECTOR of V
for w being VECTOR of CLSStruct(# D,d1,A,M #) st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * v by Lm4;