:: VECTSP10 semantic presentation

begin

definition
let K be doubleLoopStr ;
func StructVectSp K ->  strict VectSpStr over K equals :: VECTSP10:def 1
 VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #);
coherence
 VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is strict VectSpStr over K ;
end;

:: deftheorem  defines StructVectSp VECTSP10:def_1_:_
 for K being doubleLoopStr holds StructVectSp K = VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #);

registration
let K be non empty doubleLoopStr ;
cluster StructVectSp K ->  non empty strict ;
coherence
 not StructVectSp K is empty ;
end;

registration
let K be non empty Abelian doubleLoopStr ;
cluster StructVectSp K ->  Abelian strict ;
coherence
 StructVectSp K is Abelian
proof
set V = StructVectSp K;
now__::_thesis:_for_x,_y_being_Vector_of_(StructVectSp_K)_holds_x_+_y_=_y_+_x
let x, y be Vector of (StructVectSp K); ::_thesis: x + y = y + x
reconsider x9 = x, y9 = y as Element of K ;
thus x + y = y9 + x9 by RLVECT_1:2
.= y + x ; ::_thesis: verum
end;
hence  StructVectSp K is Abelian by RLVECT_1:def_2; ::_thesis: verum
end;
end;

registration
let K be non empty add-associative doubleLoopStr ;
cluster StructVectSp K ->  add-associative strict ;
coherence
 StructVectSp K is add-associative
proof
set V = StructVectSp K;
now__::_thesis:_for_x,_y,_z_being_Vector_of_(StructVectSp_K)_holds_(x_+_y)_+_z_=_x_+_(y_+_z)
let x, y, z be Vector of (StructVectSp K); ::_thesis: (x + y) + z = x + (y + z)
reconsider x9 = x, y9 = y, z9 = z as Element of K ;
thus (x + y) + z = (x9 + y9) + z9
.= x9 + (y9 + z9) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: verum
end;
hence  StructVectSp K is add-associative by RLVECT_1:def_3; ::_thesis: verum
end;
end;

registration
let K be non empty right_zeroed doubleLoopStr ;
cluster StructVectSp K ->  right_zeroed strict ;
coherence
 StructVectSp K is right_zeroed
proof
set V = StructVectSp K;
now__::_thesis:_for_x_being_Vector_of_(StructVectSp_K)_holds_x_+_(0._(StructVectSp_K))_=_x
let x be Vector of (StructVectSp K); ::_thesis: x + (0. (StructVectSp K)) = x
reconsider x9 = x as Element of K ;
thus x + (0. (StructVectSp K)) = x9 + (0. K)
.= x by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence  StructVectSp K is right_zeroed by RLVECT_1:def_4; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable doubleLoopStr ;
cluster StructVectSp K ->  right_complementable strict ;
coherence
 StructVectSp K is right_complementable
proof
set V = StructVectSp K;
let x be Vector of (StructVectSp K); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x9 = x as Element of K ;
consider t being Element of K such that
A1: x9 + t = 0. K by ALGSTR_0:def_11;
reconsider t9 = t as Vector of (StructVectSp K) ;
take  t9 ; :: according to ALGSTR_0:def_11 ::_thesis: x + t9 = 0. (StructVectSp K)
thus  x + t9 = 0. (StructVectSp K) by A1; ::_thesis: verum
end;
end;

registration
let K be non empty associative distributive left_unital doubleLoopStr ;
cluster StructVectSp K ->  strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital )
proof
set V = StructVectSp K;
now__::_thesis:_for_x,_y_being_Element_of_K
for_v,_w_being_Vector_of_(StructVectSp_K)_holds_
(_x_*_(v_+_w)_=_(x_*_v)_+_(x_*_w)_&_(x_+_y)_*_v_=_(x_*_v)_+_(y_*_v)_&_(x_*_y)_*_v_=_x_*_(y_*_v)_&_(1._K)_*_v_=_v_)
let x, y be Element of K; ::_thesis: for v, w being Vector of (StructVectSp K) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
let v, w be Vector of (StructVectSp K); ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
reconsider v9 = v, w9 = w as Element of K ;
thus x * (v + w) = x * (v9 + w9)
.= (x * v9) + (x * w9) by VECTSP_1:def_7
.= (x * v) + (x * w) ; ::_thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. K) * v = v )
thus (x + y) * v = (x + y) * v9
.= (x * v9) + (y * v9) by VECTSP_1:def_7
.= (x * v) + (y * v) ; ::_thesis: ( (x * y) * v = x * (y * v) & (1. K) * v = v )
thus (x * y) * v = (x * y) * v9
.= x * (y * v9) by GROUP_1:def_3
.= the lmult of (StructVectSp K) . (x,(y * v))
.= x * (y * v) ; ::_thesis: (1. K) * v = v
thus (1. K) * v = (1. K) * v9
.= v by VECTSP_1:def_8 ; ::_thesis: verum
end;
hence  ( StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital ) by VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17; ::_thesis: verum
end;
end;

registration
let K be non empty non degenerated doubleLoopStr ;
cluster StructVectSp K ->  non trivial strict ;
coherence
 not StructVectSp K is trivial ;
end;

registration
let K be non empty non degenerated doubleLoopStr ;
cluster non trivial for VectSpStr over K;
existence
 not for b1 being VectSpStr over K holds b1 is trivial
proof
take  StructVectSp K ; ::_thesis: not StructVectSp K is trivial
thus  not StructVectSp K is trivial ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
cluster non empty right_complementable add-associative right_zeroed strict for VectSpStr over K;
correctness
existence
ex b1 being non empty VectSpStr over K st
( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict );
proof
take  StructVectSp K ; ::_thesis: ( StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is strict )
thus  ( StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is strict ) ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr ;
cluster non empty right_complementable add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for VectSpStr over K;
correctness
existence
ex b1 being non empty VectSpStr over K st
( 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 & b1 is strict );
proof
take  StructVectSp K ; ::_thesis: ( StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital & StructVectSp K is strict )
thus  ( StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital & StructVectSp K is strict ) ; ::_thesis: verum
end;
end;

registration
let K be non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital doubleLoopStr ;
cluster non empty non trivial right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for VectSpStr over K;
existence
 ex b1 being non trivial VectSpStr over K st
( 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 & b1 is strict )
proof
take  StructVectSp K ; ::_thesis: ( StructVectSp K is Abelian & StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital & StructVectSp K is strict )
thus  ( StructVectSp K is Abelian & StructVectSp K is add-associative & StructVectSp K is right_zeroed & StructVectSp K is right_complementable & StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital & StructVectSp K is strict ) ; ::_thesis: verum
end;
end;

theorem Th1: :: VECTSP10:1
for K being non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr
for a being Element of K
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for v being Vector of V holds
( (0. K) * v = 0. V & a * (0. V) = 0. V )
proof
let F be non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr ; ::_thesis: for a being Element of F
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for v being Vector of V holds
( (0. F) * v = 0. V & a * (0. V) = 0. V )
let x be Element of F; ::_thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for v being Vector of V holds
( (0. F) * v = 0. V & x * (0. V) = 0. V )
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F; ::_thesis: for v being Vector of V holds
( (0. F) * v = 0. V & x * (0. V) = 0. V )
let v be Vector of V; ::_thesis: ( (0. F) * v = 0. V & x * (0. V) = 0. V )
v + ((0. F) * v) = ((1. F) * v) + ((0. F) * v) by VECTSP_1:def_17
.= ((1. F) + (0. F)) * v by VECTSP_1:def_15
.= (1. F) * v by RLVECT_1:4
.= v by VECTSP_1:def_17
.= v + (0. V) by RLVECT_1:4 ;
hence A1: (0. F) * v = 0. V by RLVECT_1:8; ::_thesis: x * (0. V) = 0. V
hence x * (0. V) = (x * (0. F)) * v by VECTSP_1:def_16
.= 0. V by A1, VECTSP_1:6 ;
::_thesis: verum
end;

theorem :: VECTSP10:2
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for S, T being Subspace of V
for v being Vector of V st S /\ T = (0). V & v in S & v in T holds
v = 0. V
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for S, T being Subspace of V
for v being Vector of V st S /\ T = (0). V & v in S & v in T holds
v = 0. V
let V be VectSp of K; ::_thesis: for S, T being Subspace of V
for v being Vector of V st S /\ T = (0). V & v in S & v in T holds
v = 0. V
let S, T be Subspace of V; ::_thesis: for v being Vector of V st S /\ T = (0). V & v in S & v in T holds
v = 0. V
let v be Vector of V; ::_thesis: ( S /\ T = (0). V & v in S & v in T implies v = 0. V )
assume that
A1: S /\ T = (0). V and
A2: ( v in S & v in T ) ; ::_thesis: v = 0. V
 ( v in the carrier of S & v in the carrier of T ) by A2, STRUCT_0:def_5;
then  v in the carrier of S /\ the carrier of T by XBOOLE_0:def_4;
then  v in the carrier of (S /\ T) by VECTSP_5:def_2;
then  v in {(0. V)} by A1, VECTSP_4:def_3;
hence  v = 0. V by TARSKI:def_1; ::_thesis: verum
end;

theorem Th3: :: VECTSP10:3
for K being Field
for V being VectSp of K
for x being set
for v being Vector of V holds
( x in Lin {v} iff ex a being Element of K st x = a * v )
proof
let K be Field; ::_thesis: for V being VectSp of K
for x being set
for v being Vector of V holds
( x in Lin {v} iff ex a being Element of K st x = a * v )
let V be VectSp of K; ::_thesis: for x being set
for v being Vector of V holds
( x in Lin {v} iff ex a being Element of K st x = a * v )
let x be set ; ::_thesis: for v being Vector of V holds
( x in Lin {v} iff ex a being Element of K st x = a * v )
let v be Vector of V; ::_thesis: ( x in Lin {v} iff ex a being Element of K st x = a * v )
thus  ( x in Lin {v} implies ex a being Element of K st x = a * v ) ::_thesis: ( ex a being Element of K st x = a * v implies x in Lin {v} )
proof
assume  x in Lin {v} ; ::_thesis: ex a being Element of K st x = a * v
then consider l being Linear_Combination of {v} such that
A1: x = Sum l by VECTSP_7:7;
 Sum l = (l . v) * v by VECTSP_6:17;
hence  ex a being Element of K st x = a * v by A1; ::_thesis: verum
end;
given a being Element of K such that A2: x = a * v ; ::_thesis: x in Lin {v}
deffunc H1( set ) ->  Element of the carrier of K = 0. K;
consider f being Function of the carrier of V, the carrier of K such that
A3: f . v = a and
A4: for z being Vector of V st z <> v holds
f . z = H1(z) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;
now__::_thesis:_for_z_being_Vector_of_V_st_not_z_in_{v}_holds_
f_._z_=_0._K
let z be Vector of V; ::_thesis: ( not z in {v} implies f . z = 0. K )
assume  not z in {v} ; ::_thesis: f . z = 0. K
then  z <> v by TARSKI:def_1;
hence  f . z = 0. K by A4; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
 Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume A5: x in Carrier f ; ::_thesis: x in {v}
then  f . x <> 0. K by VECTSP_6:2;
then  x = v by A4, A5;
hence  x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v} by VECTSP_6:def_4;
 Sum f = x by A2, A3, VECTSP_6:17;
hence  x in Lin {v} by VECTSP_7:7; ::_thesis: verum
end;

theorem Th4: :: VECTSP10:4
for K being Field
for V being VectSp of K
for v being Vector of V
for a, b being Scalar of st v <> 0. V & a * v = b * v holds
a = b
proof
let K be Field; ::_thesis: for V being VectSp of K
for v being Vector of V
for a, b being Scalar of st v <> 0. V & a * v = b * v holds
a = b
let V be VectSp of K; ::_thesis: for v being Vector of V
for a, b being Scalar of st v <> 0. V & a * v = b * v holds
a = b
let v be Vector of V; ::_thesis: for a, b being Scalar of st v <> 0. V & a * v = b * v holds
a = b
let a, b be Scalar of ; ::_thesis: ( v <> 0. V & a * v = b * v implies a = b )
assume that
A1: v <> 0. V and
A2: a * v = b * v ; ::_thesis: a = b
 (a * v) - (b * v) = 0. V by A2, VECTSP_1:19;
then  (a - b) * v = 0. V by VECTSP_4:82;
then  a - b = 0. K by A1, VECTSP_1:15;
hence  a = b by VECTSP_1:19; ::_thesis: verum
end;

theorem Th5: :: VECTSP10:5
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2]
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2]
let V be VectSp of K; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2]
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v, v1, v2 being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2] )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v, v1, v2 being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2]
let v, v1, v2 be Vector of V; ::_thesis: ( v1 in W1 & v2 in W2 & v = v1 + v2 implies v |-- (W1,W2) = [v1,v2] )
 ( [v1,v2] `1 = v1 & [v1,v2] `2 = v2 ) by MCART_1:7;
hence  ( v1 in W1 & v2 in W2 & v = v1 + v2 implies v |-- (W1,W2) = [v1,v2] ) by A1, VECTSP_5:def_6; ::_thesis: verum
end;

theorem Th6: :: VECTSP10:6
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2
let V be VectSp of K; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2 )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2
let v, v1, v2 be Vector of V; ::_thesis: ( v |-- (W1,W2) = [v1,v2] implies v = v1 + v2 )
assume  v |-- (W1,W2) = [v1,v2] ; ::_thesis: v = v1 + v2
then  ( (v |-- (W1,W2)) `1 = v1 & (v |-- (W1,W2)) `2 = v2 ) by MCART_1:7;
hence  v = v1 + v2 by A1, VECTSP_5:def_6; ::_thesis: verum
end;

theorem Th7: :: VECTSP10:7
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 )
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 )
let V be VectSp of K; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 )
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 ) )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 & v2 in W2 )
let v, v1, v2 be Vector of V; ::_thesis: ( v |-- (W1,W2) = [v1,v2] implies ( v1 in W1 & v2 in W2 ) )
assume  v |-- (W1,W2) = [v1,v2] ; ::_thesis: ( v1 in W1 & v2 in W2 )
then  ( (v |-- (W1,W2)) `1 = v1 & (v |-- (W1,W2)) `2 = v2 ) by MCART_1:7;
hence  ( v1 in W1 & v2 in W2 ) by A1, VECTSP_5:def_6; ::_thesis: verum
end;

theorem Th8: :: VECTSP10:8
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1]
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1]
let V be VectSp of K; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1]
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1] )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1]
let v, v1, v2 be Vector of V; ::_thesis: ( v |-- (W1,W2) = [v1,v2] implies v |-- (W2,W1) = [v2,v1] )
assume A2: v |-- (W1,W2) = [v1,v2] ; ::_thesis: v |-- (W2,W1) = [v2,v1]
then A3: (v |-- (W1,W2)) `1 = v1 by MCART_1:7;
then A4: v1 in W1 by A1, VECTSP_5:def_6;
A5: (v |-- (W1,W2)) `2 = v2 by A2, MCART_1:7;
then A6: v2 in W2 by A1, VECTSP_5:def_6;
 v = v2 + v1 by A1, A3, A5, VECTSP_5:def_6;
hence  v |-- (W2,W1) = [v2,v1] by A1, A4, A6, Th5, VECTSP_5:41; ::_thesis: verum
end;

theorem Th9: :: VECTSP10:9
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being Vector of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)]
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being Vector of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)]
let V be VectSp of K; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being Vector of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)]
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v being Vector of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)] )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v being Vector of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)]
let v be Vector of V; ::_thesis: ( v in W1 implies v |-- (W1,W2) = [v,(0. V)] )
assume A2: v in W1 ; ::_thesis: v |-- (W1,W2) = [v,(0. V)]
 ( 0. V in W2 & v + (0. V) = v ) by RLVECT_1:4, VECTSP_4:17;
hence  v |-- (W1,W2) = [v,(0. V)] by A1, A2, Th5; ::_thesis: verum
end;

theorem Th10: :: VECTSP10:10
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being Vector of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v]
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being Vector of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v]
let V be VectSp of K; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being Vector of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v]
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies for v being Vector of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v] )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: for v being Vector of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v]
let v be Vector of V; ::_thesis: ( v in W2 implies v |-- (W1,W2) = [(0. V),v] )
assume  v in W2 ; ::_thesis: v |-- (W1,W2) = [(0. V),v]
then  v |-- (W2,W1) = [v,(0. V)] by A1, Th9, VECTSP_5:41;
hence  v |-- (W1,W2) = [(0. V),v] by A1, Th8, VECTSP_5:41; ::_thesis: verum
end;

theorem Th11: :: VECTSP10:11
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for V1 being Subspace of V
for W1 being Subspace of V1
for v being Vector of V st v in W1 holds
v is Vector of V1
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for V1 being Subspace of V
for W1 being Subspace of V1
for v being Vector of V st v in W1 holds
v is Vector of V1
let V be VectSp of K; ::_thesis: for V1 being Subspace of V
for W1 being Subspace of V1
for v being Vector of V st v in W1 holds
v is Vector of V1
let V1 be Subspace of V; ::_thesis: for W1 being Subspace of V1
for v being Vector of V st v in W1 holds
v is Vector of V1
let W1 be Subspace of V1; ::_thesis: for v being Vector of V st v in W1 holds
v is Vector of V1
let v be Vector of V; ::_thesis: ( v in W1 implies v is Vector of V1 )
assume  v in W1 ; ::_thesis: v is Vector of V1
then  ( the carrier of W1 c= the carrier of V1 & v in the carrier of W1 ) by STRUCT_0:def_5, VECTSP_4:def_2;
hence  v is Vector of V1 ; ::_thesis: verum
end;

theorem Th12: :: VECTSP10:12
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for V1, V2, W being Subspace of V
for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for V1, V2, W being Subspace of V
for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
let V be VectSp of K; ::_thesis: for V1, V2, W being Subspace of V
for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
let V1, V2, W be Subspace of V; ::_thesis: for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds
W1 + W2 = V1 + V2
let W1, W2 be Subspace of W; ::_thesis: ( W1 = V1 & W2 = V2 implies W1 + W2 = V1 + V2 )
assume A1: ( W1 = V1 & W2 = V2 ) ; ::_thesis: W1 + W2 = V1 + V2
reconsider W3 = W1 + W2 as Subspace of V by VECTSP_4:26;
now__::_thesis:_for_v_being_Vector_of_V_holds_
(_(_v_in_W3_implies_v_in_V1_+_V2_)_&_(_v_in_V1_+_V2_implies_v_in_W3_)_)
let v be Vector of V; ::_thesis: ( ( v in W3 implies v in V1 + V2 ) & ( v in V1 + V2 implies v in W3 ) )
A2: ( the carrier of W1 c= the carrier of W & the carrier of W2 c= the carrier of W ) by VECTSP_4:def_2;
hereby  ::_thesis: ( v in V1 + V2 implies v in W3 )
assume A3: v in W3 ; ::_thesis: v in V1 + V2
then reconsider w = v as Vector of W by Th11;
consider w1, w2 being Vector of W such that
A4: ( w1 in W1 & w2 in W2 ) and
A5: w = w1 + w2 by A3, VECTSP_5:1;
reconsider v1 = w1, v2 = w2 as Vector of V by VECTSP_4:10;
 v = v1 + v2 by A5, VECTSP_4:13;
hence  v in V1 + V2 by A1, A4, VECTSP_5:1; ::_thesis: verum
end;
assume  v in V1 + V2 ; ::_thesis: v in W3
then consider v1, v2 being Vector of V such that
A6: ( v1 in V1 & v2 in V2 ) and
A7: v = v1 + v2 by VECTSP_5:1;
 ( v1 in the carrier of W1 & v2 in the carrier of W2 ) by A1, A6, STRUCT_0:def_5;
then reconsider w1 = v1, w2 = v2 as Vector of W by A2;
 v = w1 + w2 by A7, VECTSP_4:13;
hence  v in W3 by A1, A6, VECTSP_5:1; ::_thesis: verum
end;
hence  W1 + W2 = V1 + V2 by VECTSP_4:30; ::_thesis: verum
end;

theorem Th13: :: VECTSP10:13
for K being Field
for V being VectSp of K
for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
Lin {w} = Lin {v}
proof
let K be Field; ::_thesis: for V being VectSp of K
for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
Lin {w} = Lin {v}
let V be VectSp of K; ::_thesis: for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
Lin {w} = Lin {v}
let W be Subspace of V; ::_thesis: for v being Vector of V
for w being Vector of W st v = w holds
Lin {w} = Lin {v}
let v be Vector of V; ::_thesis: for w being Vector of W st v = w holds
Lin {w} = Lin {v}
let w be Vector of W; ::_thesis: ( v = w implies Lin {w} = Lin {v} )
assume A1: v = w ; ::_thesis: Lin {w} = Lin {v}
reconsider W1 = Lin {w} as Subspace of V by VECTSP_4:26;
now__::_thesis:_for_u_being_Vector_of_V_holds_
(_(_u_in_W1_implies_u_in_Lin_{v}_)_&_(_u_in_Lin_{v}_implies_u_in_W1_)_)
let u be Vector of V; ::_thesis: ( ( u in W1 implies u in Lin {v} ) & ( u in Lin {v} implies u in W1 ) )
hereby  ::_thesis: ( u in Lin {v} implies u in W1 )
assume  u in W1 ; ::_thesis: u in Lin {v}
then consider a being Element of K such that
A2: u = a * w by Th3;
 u = a * v by A1, A2, VECTSP_4:14;
hence  u in Lin {v} by Th3; ::_thesis: verum
end;
assume  u in Lin {v} ; ::_thesis: u in W1
then consider a being Element of K such that
A3: u = a * v by Th3;
 u = a * w by A1, A3, VECTSP_4:14;
hence  u in W1 by Th3; ::_thesis: verum
end;
hence  Lin {w} = Lin {v} by VECTSP_4:30; ::_thesis: verum
end;

theorem Th14: :: VECTSP10:14
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V st not v in X holds
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
proof
let K be Field; ::_thesis: for V being VectSp of K
for v being Vector of V
for X being Subspace of V st not v in X holds
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let V be VectSp of K; ::_thesis: for v being Vector of V
for X being Subspace of V st not v in X holds
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let v be Vector of V; ::_thesis: for X being Subspace of V st not v in X holds
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let X be Subspace of V; ::_thesis: ( not v in X implies for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y} )
assume A1: not v in X ; ::_thesis: for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let y be Vector of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & W = X implies X + (Lin {v}) is_the_direct_sum_of W, Lin {y} )
assume that
A2: v = y and
A3: W = X ; ::_thesis: X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
 Lin {v} = Lin {y} by A2, Th13;
hence  VectSpStr(# the carrier of (X + (Lin {v})), the addF of (X + (Lin {v})), the ZeroF of (X + (Lin {v})), the lmult of (X + (Lin {v})) #) = W + (Lin {y}) by A3, Th12; :: according to VECTSP_5:def_4 ::_thesis: W /\ (Lin {y}) = (0). (X + (Lin {v}))
assume  W /\ (Lin {y}) <> (0). (X + (Lin {v})) ; ::_thesis: contradiction
then consider z being Vector of (X + (Lin {v})) such that
A4: ( ( z in W /\ (Lin {y}) & not z in (0). (X + (Lin {v})) ) or ( z in (0). (X + (Lin {v})) & not z in W /\ (Lin {y}) ) ) by VECTSP_4:30;
percases ( ( z in W /\ (Lin {y}) & not z in (0). (X + (Lin {v})) ) or ( not z in W /\ (Lin {y}) & z in (0). (X + (Lin {v})) ) ) by A4;
supposethat A5: z in W /\ (Lin {y}) and
A6: not z in (0). (X + (Lin {v})) ; ::_thesis: contradiction
 z in Lin {y} by A5, VECTSP_5:3;
then consider a being Element of K such that
A7: z = a * y by Th3;
A8: z in W by A5, VECTSP_5:3;
now__::_thesis:_contradiction
percases ( a = 0. K or a <> 0. K ) ;
suppose a = 0. K ; ::_thesis: contradiction
then  z = 0. (X + (Lin {v})) by A7, VECTSP_1:15;
hence  contradiction by A6, VECTSP_4:17; ::_thesis: verum
end;
supposeA9: a <> 0. K ; ::_thesis: contradiction
y = (1_ K) * y by VECTSP_1:def_17
.= ((a ") * a) * y by A9, VECTSP_1:def_10
.= (a ") * (a * y) by VECTSP_1:def_16 ;
hence  contradiction by A1, A2, A3, A8, A7, VECTSP_4:21; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
supposethat A10: not z in W /\ (Lin {y}) and
A11: z in (0). (X + (Lin {v})) ; ::_thesis: contradiction
 z = 0. (X + (Lin {v})) by A11, VECTSP_4:35;
hence  contradiction by A10, VECTSP_4:17; ::_thesis: verum
end;
end;
end;

theorem Th15: :: VECTSP10:15
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
proof
let K be Field; ::_thesis: for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
let V be VectSp of K; ::_thesis: for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
let v be Vector of V; ::_thesis: for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
let X be Subspace of V; ::_thesis: for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
let y be Vector of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies y |-- (W,(Lin {y})) = [(0. W),y] )
assume  ( v = y & X = W & not v in X ) ; ::_thesis: y |-- (W,(Lin {y})) = [(0. W),y]
then  ( y in {y} & X + (Lin {v}) is_the_direct_sum_of W, Lin {y} ) by Th14, TARSKI:def_1;
then  y |-- (W,(Lin {y})) = [(0. (X + (Lin {v}))),y] by Th10, VECTSP_7:8;
hence  y |-- (W,(Lin {y})) = [(0. W),y] by VECTSP_4:11; ::_thesis: verum
end;

theorem Th16: :: VECTSP10:16
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
proof
let K be Field; ::_thesis: for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
let V be VectSp of K; ::_thesis: for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
let v be Vector of V; ::_thesis: for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
let X be Subspace of V; ::_thesis: for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
let y be Vector of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; ::_thesis: for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
A4: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th14;
let w be Vector of (X + (Lin {v})); ::_thesis: ( w in X implies w |-- (W,(Lin {y})) = [w,(0. V)] )
assume  w in X ; ::_thesis: w |-- (W,(Lin {y})) = [w,(0. V)]
then  w |-- (W,(Lin {y})) = [w,(0. (X + (Lin {v})))] by A2, A4, Th9;
hence  w |-- (W,(Lin {y})) = [w,(0. V)] by VECTSP_4:11; ::_thesis: verum
end;

theorem Th17: :: VECTSP10:17
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for v being Vector of V
for W1, W2 being Subspace of V ex v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2]
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for v being Vector of V
for W1, W2 being Subspace of V ex v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2]
let V be VectSp of K; ::_thesis: for v being Vector of V
for W1, W2 being Subspace of V ex v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2]
let v be Vector of V; ::_thesis: for W1, W2 being Subspace of V ex v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2]
let W1, W2 be Subspace of V; ::_thesis: ex v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2]
take  (v |-- (W1,W2)) `1 ; ::_thesis: ex v2 being Vector of V st v |-- (W1,W2) = [((v |-- (W1,W2)) `1),v2]
take  (v |-- (W1,W2)) `2 ; ::_thesis: v |-- (W1,W2) = [((v |-- (W1,W2)) `1),((v |-- (W1,W2)) `2)]
thus  v |-- (W1,W2) = [((v |-- (W1,W2)) `1),((v |-- (W1,W2)) `2)] by MCART_1:21; ::_thesis: verum
end;

theorem Th18: :: VECTSP10:18
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
proof
let K be Field; ::_thesis: for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
let V be VectSp of K; ::_thesis: for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
let v be Vector of V; ::_thesis: for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
let X be Subspace of V; ::_thesis: for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
let y be Vector of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; ::_thesis: for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
let w be Vector of (X + (Lin {v})); ::_thesis: ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
consider v1, v2 being Vector of (X + (Lin {v})) such that
A4: w |-- (W,(Lin {y})) = [v1,v2] by Th17;
A5: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th14;
then  v1 in W by A4, Th7;
then reconsider x = v1 as Vector of X by A2, STRUCT_0:def_5;
 v2 in Lin {y} by A5, A4, Th7;
then consider r being Element of K such that
A6: v2 = r * y by Th3;
take  x ; ::_thesis: ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
take  r ; ::_thesis: w |-- (W,(Lin {y})) = [x,(r * v)]
thus  w |-- (W,(Lin {y})) = [x,(r * v)] by A1, A4, A6, VECTSP_4:14; ::_thesis: verum
end;

theorem Th19: :: VECTSP10:19
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
proof
let K be Field; ::_thesis: for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let V be VectSp of K; ::_thesis: for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let v be Vector of V; ::_thesis: for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let X be Subspace of V; ::_thesis: for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let y be Vector of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies for w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; ::_thesis: for w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
A4: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th14;
let w1, w2 be Vector of (X + (Lin {v})); ::_thesis: for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let x1, x2 be Vector of X; ::_thesis: for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
let r1, r2 be Element of K; ::_thesis: ( w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] implies (w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)] )
assume that
A5: w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] and
A6: w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] ; ::_thesis: (w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
reconsider y1 = x1, y2 = x2 as Vector of (X + (Lin {v})) by A2, VECTSP_4:10;
A7: r2 * v = r2 * y by A1, VECTSP_4:14;
then A8: y2 in W by A4, A6, Th7;
 (r1 + r2) * v = (r1 + r2) * y by A1, VECTSP_4:14;
then A9: (r1 + r2) * v in Lin {y} by Th3;
reconsider z1 = x1, z2 = x2 as Vector of V by VECTSP_4:10;
A10: y1 + y2 = z1 + z2 by VECTSP_4:13
.= x1 + x2 by VECTSP_4:13 ;
A11: r1 * v = r1 * y by A1, VECTSP_4:14;
then  y1 in W by A4, A5, Th7;
then A12: y1 + y2 in W by A8, VECTSP_4:20;
A13: w2 = y2 + (r2 * y) by A4, A6, A7, Th6;
 w1 = y1 + (r1 * y) by A4, A5, A11, Th6;
then A14: w1 + w2 = ((y1 + (r1 * y)) + y2) + (r2 * y) by A13, RLVECT_1:def_3
.= ((y1 + y2) + (r1 * y)) + (r2 * y) by RLVECT_1:def_3
.= (y1 + y2) + ((r1 * y) + (r2 * y)) by RLVECT_1:def_3
.= (y1 + y2) + ((r1 + r2) * y) by VECTSP_1:def_15 ;
 (r1 + r2) * y = (r1 + r2) * v by A1, VECTSP_4:14;
hence  (w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)] by A4, A12, A9, A14, A10, Th5; ::_thesis: verum
end;

theorem Th20: :: VECTSP10:20
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
proof
let K be Field; ::_thesis: for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let V be VectSp of K; ::_thesis: for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let v be Vector of V; ::_thesis: for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let X be Subspace of V; ::_thesis: for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let y be Vector of (X + (Lin {v})); ::_thesis: for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let W be Subspace of X + (Lin {v}); ::_thesis: ( v = y & X = W & not v in X implies for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)] )
assume that
A1: v = y and
A2: X = W and
A3: not v in X ; ::_thesis: for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
A4: X + (Lin {v}) is_the_direct_sum_of W, Lin {y} by A1, A2, A3, Th14;
let w be Vector of (X + (Lin {v})); ::_thesis: for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let x be Vector of X; ::_thesis: for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
let t, r be Element of K; ::_thesis: ( w |-- (W,(Lin {y})) = [x,(r * v)] implies (t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)] )
assume A5: w |-- (W,(Lin {y})) = [x,(r * v)] ; ::_thesis: (t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
reconsider z = x as Vector of (X + (Lin {v})) by A2, VECTSP_4:10;
 r * y = r * v by A1, VECTSP_4:14;
then A6: t * w = t * (z + (r * y)) by A4, A5, Th6
.= (t * z) + (t * (r * y)) by VECTSP_1:def_14
.= (t * z) + ((t * r) * y) by VECTSP_1:def_16 ;
reconsider u = x as Vector of V by VECTSP_4:10;
A7: (t * r) * y in Lin {y} by Th3;
A8: (t * r) * y = (t * r) * v by A1, VECTSP_4:14;
A9: t * z = t * u by VECTSP_4:14
.= t * x by VECTSP_4:14 ;
then  t * z in W by A2, STRUCT_0:def_5;
hence  (t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)] by A4, A9, A8, A7, A6, Th5; ::_thesis: verum
end;

begin

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be Subspace of V;
func CosetSet (V,W) ->  non empty Subset-Family of V equals :: VECTSP10:def 2
 {  A where A is Coset of W : verum  }  ;
correctness
coherence
{  A where A is Coset of W : verum  }  is non empty Subset-Family of V;
proof
set C =  {  A where A is Coset of W : verum  }  ;
A1:  {  A where A is Coset of W : verum  }  c= bool the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Coset of W : verum  }  or x in bool the carrier of V )
assume  x in  {  A where A is Coset of W : verum  }  ; ::_thesis: x in bool the carrier of V
then  ex A being Coset of W st A = x ;
hence  x in bool the carrier of V ; ::_thesis: verum
end;
 the carrier of W is Coset of W by VECTSP_4:73;
then  the carrier of W in  {  A where A is Coset of W : verum  }  ;
hence   {  A where A is Coset of W : verum  }  is non empty Subset-Family of V by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines CosetSet VECTSP10:def_2_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V holds CosetSet (V,W) =  {  A where A is Coset of W : verum  }  ;

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be Subspace of V;
func addCoset (V,W) ->  BinOp of (CosetSet (V,W)) means :Def3: :: VECTSP10:def 3
 for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
it . (A,B) = (a + b) + W;
existence
 ex b1 being BinOp of (CosetSet (V,W)) st
for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
b1 . (A,B) = (a + b) + W
proof
defpred S1[ set , set , set ] means  for a, b being Vector of V st $1 = a + W & $2 = b + W holds
$3 = (a + b) + W;
set C = CosetSet (V,W);
A1: now__::_thesis:_for_A,_B_being_Element_of_CosetSet_(V,W)_ex_z_being_Element_of_CosetSet_(V,W)_st_S1[A,B,z]
let A, B be Element of CosetSet (V,W); ::_thesis: ex z being Element of CosetSet (V,W) st S1[A,B,z]
 A in CosetSet (V,W) ;
then consider A1 being Coset of W such that
A2: A1 = A ;
consider a being Vector of V such that
A3: A1 = a + W by VECTSP_4:def_6;
 B in CosetSet (V,W) ;
then consider B1 being Coset of W such that
A4: B1 = B ;
consider b being Vector of V such that
A5: B1 = b + W by VECTSP_4:def_6;
reconsider z = (a + b) + W as Coset of W by VECTSP_4:def_6;
 z in CosetSet (V,W) ;
then reconsider z = z as Element of CosetSet (V,W) ;
take z = z; ::_thesis: S1[A,B,z]
thus  S1[A,B,z] ::_thesis: verum
proof
let a1, b1 be Vector of V; ::_thesis: ( A = a1 + W & B = b1 + W implies z = (a1 + b1) + W )
assume that
A6: A = a1 + W and
A7: B = b1 + W ; ::_thesis: z = (a1 + b1) + W
 a1 in a + W by A2, A3, A6, VECTSP_4:44;
then consider w1 being Vector of V such that
A8: w1 in W and
A9: a1 = a + w1 by VECTSP_4:42;
 b1 in b + W by A4, A5, A7, VECTSP_4:44;
then consider w2 being Vector of V such that
A10: w2 in W and
A11: b1 = b + w2 by VECTSP_4:42;
A12: w1 + w2 in W by A8, A10, VECTSP_4:20;
a1 + b1 = ((w1 + a) + b) + w2 by A9, A11, RLVECT_1:def_3
.= (w1 + (a + b)) + w2 by RLVECT_1:def_3
.= (a + b) + (w1 + w2) by RLVECT_1:def_3 ;
then A13: a1 + b1 in (a + b) + W by A12;
 a1 + b1 in (a1 + b1) + W by VECTSP_4:44;
hence  z = (a1 + b1) + W by A13, VECTSP_4:56; ::_thesis: verum
end;
end;
consider f being Function of [:(CosetSet (V,W)),(CosetSet (V,W)):],(CosetSet (V,W)) such that
A14: for A, B being Element of CosetSet (V,W) holds S1[A,B,f . (A,B)] from BINOP_1:sch_3(A1);
reconsider f = f as BinOp of (CosetSet (V,W)) ;
take  f ; ::_thesis: for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f . (A,B) = (a + b) + W
let A, B be Element of CosetSet (V,W); ::_thesis: for a, b being Vector of V st A = a + W & B = b + W holds
f . (A,B) = (a + b) + W
let a, b be Vector of V; ::_thesis: ( A = a + W & B = b + W implies f . (A,B) = (a + b) + W )
assume  ( A = a + W & B = b + W ) ; ::_thesis: f . (A,B) = (a + b) + W
hence  f . (A,B) = (a + b) + W by A14; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (CosetSet (V,W)) st ( for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
b1 . (A,B) = (a + b) + W ) & ( for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
b2 . (A,B) = (a + b) + W ) holds
b1 = b2
proof
set C = CosetSet (V,W);
let f1, f2 be BinOp of (CosetSet (V,W)); ::_thesis: ( ( for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f1 . (A,B) = (a + b) + W ) & ( for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f2 . (A,B) = (a + b) + W ) implies f1 = f2 )
assume that
A15: for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f1 . (A,B) = (a + b) + W and
A16: for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
f2 . (A,B) = (a + b) + W ; ::_thesis: f1 = f2
now__::_thesis:_for_A,_B_being_Element_of_CosetSet_(V,W)_holds_f1_._(A,B)_=_f2_._(A,B)
let A, B be Element of CosetSet (V,W); ::_thesis: f1 . (A,B) = f2 . (A,B)
 A in CosetSet (V,W) ;
then consider A1 being Coset of W such that
A17: A1 = A ;
consider a being Vector of V such that
A18: A1 = a + W by VECTSP_4:def_6;
 B in CosetSet (V,W) ;
then consider B1 being Coset of W such that
A19: B1 = B ;
consider b being Vector of V such that
A20: B1 = b + W by VECTSP_4:def_6;
thus f1 . (A,B) = (a + b) + W by A15, A17, A19, A18, A20
.= f2 . (A,B) by A16, A17, A19, A18, A20 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines addCoset VECTSP10:def_3_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for b4 being BinOp of (CosetSet (V,W)) holds
( b4 = addCoset (V,W) iff for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
b4 . (A,B) = (a + b) + W );

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be Subspace of V;
func zeroCoset (V,W) ->  Element of CosetSet (V,W) equals :: VECTSP10:def 4
 the carrier of W;
coherence
 the carrier of W is Element of CosetSet (V,W)
proof
 the carrier of W = (0. V) + W by VECTSP_4:45;
then  the carrier of W is Coset of W by VECTSP_4:def_6;
then  the carrier of W in CosetSet (V,W) ;
hence  the carrier of W is Element of CosetSet (V,W) ; ::_thesis: verum
end;
end;

:: deftheorem  defines zeroCoset VECTSP10:def_4_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V holds zeroCoset (V,W) = the carrier of W;

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be Subspace of V;
func lmultCoset (V,W) ->  Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) means :Def5: :: VECTSP10:def 5
 for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
it . (z,A) = (z * a) + W;
existence
 ex b1 being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) st
for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
b1 . (z,A) = (z * a) + W
proof
defpred S1[ Element of K, set , set ] means  for a being Vector of V st $2 = a + W holds
$3 = ($1 * a) + W;
set cF = the carrier of K;
set C = CosetSet (V,W);
A1: now__::_thesis:_for_z_being_Element_of_K
for_A_being_Element_of_CosetSet_(V,W)_ex_c_being_Element_of_CosetSet_(V,W)_st_S1[z,A,c]
let z be Element of K; ::_thesis: for A being Element of CosetSet (V,W) ex c being Element of CosetSet (V,W) st S1[z,A,c]
let A be Element of CosetSet (V,W); ::_thesis: ex c being Element of CosetSet (V,W) st S1[z,A,c]
 A in CosetSet (V,W) ;
then consider A1 being Coset of W such that
A2: A1 = A ;
consider a being Vector of V such that
A3: A1 = a + W by VECTSP_4:def_6;
reconsider c = (z * a) + W as Coset of W by VECTSP_4:def_6;
 c in CosetSet (V,W) ;
then reconsider c = c as Element of CosetSet (V,W) ;
take c = c; ::_thesis: S1[z,A,c]
thus  S1[z,A,c] ::_thesis: verum
proof
let a1 be Vector of V; ::_thesis: ( A = a1 + W implies c = (z * a1) + W )
assume  A = a1 + W ; ::_thesis: c = (z * a1) + W
then  a1 in a + W by A2, A3, VECTSP_4:44;
then consider w1 being Vector of V such that
A4: ( w1 in W & a1 = a + w1 ) by VECTSP_4:42;
 ( z * a1 = (z * a) + (z * w1) & z * w1 in W ) by A4, VECTSP_1:def_14, VECTSP_4:21;
then A5: z * a1 in (z * a) + W ;
 z * a1 in (z * a1) + W by VECTSP_4:44;
hence  c = (z * a1) + W by A5, VECTSP_4:56; ::_thesis: verum
end;
end;
consider f being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) such that
A6: for z being Element of K
for A being Element of CosetSet (V,W) holds S1[z,A,f . (z,A)] from BINOP_1:sch_3(A1);
take  f ; ::_thesis: for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f . (z,A) = (z * a) + W
let z be Element of K; ::_thesis: for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f . (z,A) = (z * a) + W
let A be Element of CosetSet (V,W); ::_thesis: for a being Vector of V st A = a + W holds
f . (z,A) = (z * a) + W
let a be Vector of V; ::_thesis: ( A = a + W implies f . (z,A) = (z * a) + W )
assume  A = a + W ; ::_thesis: f . (z,A) = (z * a) + W
hence  f . (z,A) = (z * a) + W by A6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) st ( for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
b1 . (z,A) = (z * a) + W ) & ( for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
b2 . (z,A) = (z * a) + W ) holds
b1 = b2
proof
set cF = the carrier of K;
set C = CosetSet (V,W);
let f1, f2 be Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)); ::_thesis: ( ( for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f1 . (z,A) = (z * a) + W ) & ( for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f2 . (z,A) = (z * a) + W ) implies f1 = f2 )
assume that
A7: for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f1 . (z,A) = (z * a) + W and
A8: for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
f2 . (z,A) = (z * a) + W ; ::_thesis: f1 = f2
set C = CosetSet (V,W);
now__::_thesis:_for_z_being_Element_of_K
for_A_being_Element_of_CosetSet_(V,W)_holds_f1_._(z,A)_=_f2_._(z,A)
let z be Element of K; ::_thesis: for A being Element of CosetSet (V,W) holds f1 . (z,A) = f2 . (z,A)
let A be Element of CosetSet (V,W); ::_thesis: f1 . (z,A) = f2 . (z,A)
 A in CosetSet (V,W) ;
then consider A1 being Coset of W such that
A9: A1 = A ;
consider a being Vector of V such that
A10: A1 = a + W by VECTSP_4:def_6;
thus f1 . (z,A) = (z * a) + W by A7, A9, A10
.= f2 . (z,A) by A8, A9, A10 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines lmultCoset VECTSP10:def_5_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for b4 being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) holds
( b4 = lmultCoset (V,W) iff for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
b4 . (z,A) = (z * a) + W );

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be Subspace of V;
func VectQuot (V,W) ->  non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K means :Def6: :: VECTSP10:def 6
( the carrier of it = CosetSet (V,W) & the addF of it = addCoset (V,W) & 0. it = zeroCoset (V,W) & the lmult of it = lmultCoset (V,W) );
existence
 ex b1 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K st
( the carrier of b1 = CosetSet (V,W) & the addF of b1 = addCoset (V,W) & 0. b1 = zeroCoset (V,W) & the lmult of b1 = lmultCoset (V,W) )
proof
set C = CosetSet (V,W);
set aC = addCoset (V,W);
set zC = zeroCoset (V,W);
set lC = lmultCoset (V,W);
set A = VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #);
A1: VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is right_zeroed
proof
let A1 be Element of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #); :: according to RLVECT_1:def_4 ::_thesis: A1 + (0. VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #)) = A1
 A1 in CosetSet (V,W) ;
then consider aa being Coset of W such that
A2: A1 = aa ;
consider a being Vector of V such that
A3: aa = a + W by VECTSP_4:def_6;
 0. VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) = (0. V) + W by VECTSP_4:45;
hence A1 + (0. VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #)) = (a + (0. V)) + W by A2, A3, Def3
.= A1 by A2, A3, RLVECT_1:4 ;
::_thesis: verum
end;
A4: VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is right_complementable
proof
let A1 be Element of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #); :: according to ALGSTR_0:def_16 ::_thesis: A1 is right_complementable
A5: 0. VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) = (0. V) + W by VECTSP_4:45;
 A1 in CosetSet (V,W) ;
then consider aa being Coset of W such that
A6: A1 = aa ;
consider a being Vector of V such that
A7: aa = a + W by VECTSP_4:def_6;
set A2 = (- a) + W;
 (- a) + W is Coset of W by VECTSP_4:def_6;
then  (- a) + W in CosetSet (V,W) ;
then reconsider A2 = (- a) + W as Element of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) ;
take  A2 ; :: according to ALGSTR_0:def_11 ::_thesis: A1 + A2 = 0. VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #)
thus A1 + A2 = (a + (- a)) + W by A6, A7, Def3
.= 0. VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) by A5, RLVECT_1:5 ; ::_thesis: verum
end;
A8: now__::_thesis:_for_x,_y_being_Element_of_K
for_A1,_A2_being_Element_of_VectSpStr(#_(CosetSet_(V,W)),(addCoset_(V,W)),(zeroCoset_(V,W)),(lmultCoset_(V,W))_#)_holds_
(_x_*_(A1_+_A2)_=_(x_*_A1)_+_(x_*_A2)_&_(x_+_y)_*_A1_=_(x_*_A1)_+_(y_*_A1)_&_(x_*_y)_*_A1_=_x_*_(y_*_A1)_&_(1__K)_*_A1_=_A1_)
let x, y be Element of K; ::_thesis: for A1, A2 being Element of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) holds
( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )
let A1, A2 be Element of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #); ::_thesis: ( x * (A1 + A2) = (x * A1) + (x * A2) & (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )
 A1 in CosetSet (V,W) ;
then consider aa being Coset of W such that
A9: A1 = aa ;
 A2 in CosetSet (V,W) ;
then consider bb being Coset of W such that
A10: A2 = bb ;
consider b being Vector of V such that
A11: bb = b + W by VECTSP_4:def_6;
A12: ( (lmultCoset (V,W)) . (x,A2) = x * A2 & (lmultCoset (V,W)) . (x,A2) = (x * b) + W ) by A10, A11, Def5;
consider a being Vector of V such that
A13: aa = a + W by VECTSP_4:def_6;
A14: (addCoset (V,W)) . (A1,A2) = (a + b) + W by A9, A10, A13, A11, Def3;
A15: (lmultCoset (V,W)) . (x,A1) = (x * a) + W by A9, A13, Def5;
thus x * (A1 + A2) = (lmultCoset (V,W)) . (x,( the addF of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) . (A1,A2)))
.= (x * (a + b)) + W by A14, Def5
.= ((x * a) + (x * b)) + W by VECTSP_1:def_14
.= (x * A1) + (x * A2) by A15, A12, Def3 ; ::_thesis: ( (x + y) * A1 = (x * A1) + (y * A1) & (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )
A16: (lmultCoset (V,W)) . (y,A1) = (y * a) + W by A9, A13, Def5;
thus (x + y) * A1 = the lmult of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) . ((x + y),A1)
.= ((x + y) * a) + W by A9, A13, Def5
.= ((x * a) + (y * a)) + W by VECTSP_1:def_15
.= (x * A1) + (y * A1) by A15, A16, Def3 ; ::_thesis: ( (x * y) * A1 = x * (y * A1) & (1_ K) * A1 = A1 )
thus (x * y) * A1 = the lmult of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) . ((x * y),A1)
.= ((x * y) * a) + W by A9, A13, Def5
.= (x * (y * a)) + W by VECTSP_1:def_16
.= (lmultCoset (V,W)) . (x,(y * A1)) by A16, Def5
.= x * (y * A1) ; ::_thesis: (1_ K) * A1 = A1
thus (1_ K) * A1 = the lmult of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) . ((1_ K),A1)
.= ((1_ K) * a) + W by A9, A13, Def5
.= A1 by A9, A13, VECTSP_1:def_17 ; ::_thesis: verum
end;
A17: VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is Abelian
proof
let A1, A2 be Element of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #); :: according to RLVECT_1:def_2 ::_thesis: A1 + A2 = A2 + A1
 A1 in CosetSet (V,W) ;
then consider aa being Coset of W such that
A18: A1 = aa ;
consider a being Vector of V such that
A19: aa = a + W by VECTSP_4:def_6;
 A2 in CosetSet (V,W) ;
then consider bb being Coset of W such that
A20: A2 = bb ;
consider b being Vector of V such that
A21: bb = b + W by VECTSP_4:def_6;
thus A1 + A2 = (a + b) + W by A18, A20, A19, A21, Def3
.= A2 + A1 by A18, A20, A19, A21, Def3 ; ::_thesis: verum
end;
 VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) is add-associative
proof
let A1, A2, A3 be Element of VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #); :: according to RLVECT_1:def_3 ::_thesis: (A1 + A2) + A3 = A1 + (A2 + A3)
 A1 in CosetSet (V,W) ;
then consider aa being Coset of W such that
A22: A1 = aa ;
consider a being Vector of V such that
A23: aa = a + W by VECTSP_4:def_6;
 A2 in CosetSet (V,W) ;
then consider bb being Coset of W such that
A24: A2 = bb ;
consider b being Vector of V such that
A25: bb = b + W by VECTSP_4:def_6;
 A3 in CosetSet (V,W) ;
then consider cc being Coset of W such that
A26: A3 = cc ;
consider c being Vector of V such that
A27: cc = c + W by VECTSP_4:def_6;
A28: (addCoset (V,W)) . (A2,A3) = (b + c) + W by A24, A26, A25, A27, Def3;
 (addCoset (V,W)) . (A1,A2) = (a + b) + W by A22, A24, A23, A25, Def3;
hence (A1 + A2) + A3 = ((a + b) + c) + W by A26, A27, Def3
.= (a + (b + c)) + W by RLVECT_1:def_3
.= A1 + (A2 + A3) by A22, A23, A28, Def3 ;
::_thesis: verum
end;
then reconsider A = VectSpStr(# (CosetSet (V,W)),(addCoset (V,W)),(zeroCoset (V,W)),(lmultCoset (V,W)) #) as non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K by A17, A1, A4, A8, VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17;
take  A ; ::_thesis: ( the carrier of A = CosetSet (V,W) & the addF of A = addCoset (V,W) & 0. A = zeroCoset (V,W) & the lmult of A = lmultCoset (V,W) )
thus  ( the carrier of A = CosetSet (V,W) & the addF of A = addCoset (V,W) & 0. A = zeroCoset (V,W) & the lmult of A = lmultCoset (V,W) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K st the carrier of b1 = CosetSet (V,W) & the addF of b1 = addCoset (V,W) & 0. b1 = zeroCoset (V,W) & the lmult of b1 = lmultCoset (V,W) & the carrier of b2 = CosetSet (V,W) & the addF of b2 = addCoset (V,W) & 0. b2 = zeroCoset (V,W) & the lmult of b2 = lmultCoset (V,W) holds
b1 = b2 ;
end;

:: deftheorem Def6 defines VectQuot VECTSP10:def_6_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for b4 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K holds
( b4 = VectQuot (V,W) iff ( the carrier of b4 = CosetSet (V,W) & the addF of b4 = addCoset (V,W) & 0. b4 = zeroCoset (V,W) & the lmult of b4 = lmultCoset (V,W) ) );

theorem Th21: :: VECTSP10:21
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V holds
( zeroCoset (V,W) = (0. V) + W & 0. (VectQuot (V,W)) = zeroCoset (V,W) )
proof
let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of F
for W being Subspace of V holds
( zeroCoset (V,W) = (0. V) + W & 0. (VectQuot (V,W)) = zeroCoset (V,W) )
let V be VectSp of F; ::_thesis: for W being Subspace of V holds
( zeroCoset (V,W) = (0. V) + W & 0. (VectQuot (V,W)) = zeroCoset (V,W) )
let W be Subspace of V; ::_thesis: ( zeroCoset (V,W) = (0. V) + W & 0. (VectQuot (V,W)) = zeroCoset (V,W) )
 ( 0. V = 0. W & 0. W in W ) by STRUCT_0:def_5, VECTSP_4:11;
hence  zeroCoset (V,W) = (0. V) + W by VECTSP_4:49; ::_thesis: 0. (VectQuot (V,W)) = zeroCoset (V,W)
thus  0. (VectQuot (V,W)) = zeroCoset (V,W) by Def6; ::_thesis: verum
end;

theorem Th22: :: VECTSP10:22
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for w being Vector of (VectQuot (V,W)) holds
( w is Coset of W & ex v being Vector of V st w = v + W )
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W being Subspace of V
for w being Vector of (VectQuot (V,W)) holds
( w is Coset of W & ex v being Vector of V st w = v + W )
let V be VectSp of K; ::_thesis: for W being Subspace of V
for w being Vector of (VectQuot (V,W)) holds
( w is Coset of W & ex v being Vector of V st w = v + W )
let W be Subspace of V; ::_thesis: for w being Vector of (VectQuot (V,W)) holds
( w is Coset of W & ex v being Vector of V st w = v + W )
let w be Vector of (VectQuot (V,W)); ::_thesis: ( w is Coset of W & ex v being Vector of V st w = v + W )
set qv = VectQuot (V,W);
set cs = CosetSet (V,W);
 CosetSet (V,W) = the carrier of (VectQuot (V,W)) by Def6;
then  w in  {  A where A is Coset of W : verum  }  ;
then  ex A being Coset of W st A = w ;
hence  ( w is Coset of W & ex v being Vector of V st w = v + W ) by VECTSP_4:def_6; ::_thesis: verum
end;

theorem Th23: :: VECTSP10:23
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for v being Vector of V holds
( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W being Subspace of V
for v being Vector of V holds
( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )
let V be VectSp of K; ::_thesis: for W being Subspace of V
for v being Vector of V holds
( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )
let W be Subspace of V; ::_thesis: for v being Vector of V holds
( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )
let v be Vector of V; ::_thesis: ( v + W is Coset of W & v + W is Vector of (VectQuot (V,W)) )
set cs = CosetSet (V,W);
thus  v + W is Coset of W by VECTSP_4:def_6; ::_thesis: v + W is Vector of (VectQuot (V,W))
then  v + W in CosetSet (V,W) ;
hence  v + W is Vector of (VectQuot (V,W)) by Def6; ::_thesis: verum
end;

theorem :: VECTSP10:24
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for A being Coset of W holds A is Vector of (VectQuot (V,W))
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W being Subspace of V
for A being Coset of W holds A is Vector of (VectQuot (V,W))
let V be VectSp of K; ::_thesis: for W being Subspace of V
for A being Coset of W holds A is Vector of (VectQuot (V,W))
let W be Subspace of V; ::_thesis: for A being Coset of W holds A is Vector of (VectQuot (V,W))
let A be Coset of W; ::_thesis: A is Vector of (VectQuot (V,W))
set cs = CosetSet (V,W);
 A in CosetSet (V,W) ;
hence  A is Vector of (VectQuot (V,W)) by Def6; ::_thesis: verum
end;

theorem :: VECTSP10:25
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for A being Vector of (VectQuot (V,W))
for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W being Subspace of V
for A being Vector of (VectQuot (V,W))
for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
let V be VectSp of K; ::_thesis: for W being Subspace of V
for A being Vector of (VectQuot (V,W))
for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
let W be Subspace of V; ::_thesis: for A being Vector of (VectQuot (V,W))
for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
set vw = VectQuot (V,W);
set lm = the lmult of (VectQuot (V,W));
let A be Vector of (VectQuot (V,W)); ::_thesis: for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
let v be Vector of V; ::_thesis: for a being Scalar of st A = v + W holds
a * A = (a * v) + W
let a be Scalar of ; ::_thesis: ( A = v + W implies a * A = (a * v) + W )
assume A1: A = v + W ; ::_thesis: a * A = (a * v) + W
 A is Coset of W by Th22;
then  A in  {  B where B is Coset of W : verum  }  ;
then reconsider w = A as Element of CosetSet (V,W) ;
thus a * A = the lmult of (VectQuot (V,W)) . (a,A)
.= (lmultCoset (V,W)) . (a,w) by Def6
.= (a * v) + W by A1, Def5 ; ::_thesis: verum
end;

theorem :: VECTSP10:26
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for A1, A2 being Vector of (VectQuot (V,W))
for v1, v2 being Vector of V st A1 = v1 + W & A2 = v2 + W holds
A1 + A2 = (v1 + v2) + W
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W being Subspace of V
for A1, A2 being Vector of (VectQuot (V,W))
for v1, v2 being Vector of V st A1 = v1 + W & A2 = v2 + W holds
A1 + A2 = (v1 + v2) + W
let V be VectSp of K; ::_thesis: for W being Subspace of V
for A1, A2 being Vector of (VectQuot (V,W))
for v1, v2 being Vector of V st A1 = v1 + W & A2 = v2 + W holds
A1 + A2 = (v1 + v2) + W
let W be Subspace of V; ::_thesis: for A1, A2 being Vector of (VectQuot (V,W))
for v1, v2 being Vector of V st A1 = v1 + W & A2 = v2 + W holds
A1 + A2 = (v1 + v2) + W
set vw = VectQuot (V,W);
let A1, A2 be Vector of (VectQuot (V,W)); ::_thesis: for v1, v2 being Vector of V st A1 = v1 + W & A2 = v2 + W holds
A1 + A2 = (v1 + v2) + W
let v1, v2 be Vector of V; ::_thesis: ( A1 = v1 + W & A2 = v2 + W implies A1 + A2 = (v1 + v2) + W )
assume A1: ( A1 = v1 + W & A2 = v2 + W ) ; ::_thesis: A1 + A2 = (v1 + v2) + W
 A2 is Coset of W by Th22;
then A2: A2 in  {  B where B is Coset of W : verum  }  ;
 A1 is Coset of W by Th22;
then  A1 in  {  B where B is Coset of W : verum  }  ;
then reconsider w1 = A1, w2 = A2 as Element of CosetSet (V,W) by A2;
thus A1 + A2 = (addCoset (V,W)) . (w1,w2) by Def6
.= (v1 + v2) + W by A1, Def3 ; ::_thesis: verum
end;

begin

theorem Th27: :: VECTSP10:27
for K being Field
for V being VectSp of K
for X being Subspace of V
for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
proof
let K be Field; ::_thesis: for V being VectSp of K
for X being Subspace of V
for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let V be VectSp of K; ::_thesis: for X being Subspace of V
for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let X be Subspace of V; ::_thesis: for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let fi be linear-Functional of X; ::_thesis: for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let v be Vector of V; ::_thesis: for y being Vector of (X + (Lin {v})) st v = y & not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
let y be Vector of (X + (Lin {v})); ::_thesis: ( v = y & not v in X implies for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r ) )
assume that
A1: v = y and
A2: not v in X ; ::_thesis: for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
reconsider W1 = X as Subspace of X + (Lin {v}) by VECTSP_5:7;
let r be Element of K; ::_thesis: ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & psi . y = r )
defpred S1[ Element of (X + (Lin {v})), Element of K] means  for x being Vector of X
for s being Element of K st ($1 |-- (W1,(Lin {y}))) `1 = x & ($1 |-- (W1,(Lin {y}))) `2 = s * v holds
$2 = (fi . x) + (s * r);
A3: for e being Element of (X + (Lin {v})) ex a being Element of K st S1[e,a]
proof
let e be Element of (X + (Lin {v})); ::_thesis: ex a being Element of K st S1[e,a]
consider x being Vector of X, s being Element of K such that
A4: e |-- (W1,(Lin {y})) = [x,(s * v)] by A1, A2, Th18;
take  (fi . x) + (s * r) ; ::_thesis: S1[e,(fi . x) + (s * r)]
let x9 be Vector of X; ::_thesis: for s being Element of K st (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = s * v holds
(fi . x) + (s * r) = (fi . x9) + (s * r)
let t be Element of K; ::_thesis: ( (e |-- (W1,(Lin {y}))) `1 = x9 & (e |-- (W1,(Lin {y}))) `2 = t * v implies (fi . x) + (s * r) = (fi . x9) + (t * r) )
assume that
A5: (e |-- (W1,(Lin {y}))) `1 = x9 and
A6: (e |-- (W1,(Lin {y}))) `2 = t * v ; ::_thesis: (fi . x) + (s * r) = (fi . x9) + (t * r)
 v <> 0. V by A2, VECTSP_4:17;
then  t = s by A4, A6, Th4, MCART_1:7;
hence  (fi . x) + (s * r) = (fi . x9) + (t * r) by A4, A5, MCART_1:7; ::_thesis: verum
end;
consider f being Function of the carrier of (X + (Lin {v})), the carrier of K such that
A7: for e being Element of (X + (Lin {v})) holds S1[e,f . e] from FUNCT_2:sch_3(A3);
A8: now__::_thesis:_for_a_being_set_st_a_in_dom_fi_holds_
fi_._a_=_f_._a
let a be set ; ::_thesis: ( a in dom fi implies fi . a = f . a )
assume  a in dom fi ; ::_thesis: fi . a = f . a
then reconsider x = a as Vector of X ;
 X is Subspace of X + (Lin {v}) by VECTSP_5:7;
then  the carrier of X c= the carrier of (X + (Lin {v})) by VECTSP_4:def_2;
then reconsider v1 = x as Vector of (X + (Lin {v})) by TARSKI:def_3;
 v1 in X by STRUCT_0:def_5;
then v1 |-- (W1,(Lin {y})) = [v1,(0. V)] by A1, A2, Th16
.= [v1,((0. K) * v)] by Th1 ;
then A9: ( (v1 |-- (W1,(Lin {y}))) `1 = x & (v1 |-- (W1,(Lin {y}))) `2 = (0. K) * v ) by MCART_1:7;
thus fi . a = (fi . x) + (0. K) by RLVECT_1:4
.= (fi . x) + ((0. K) * r) by VECTSP_1:7
.= f . a by A7, A9 ; ::_thesis: verum
end;
reconsider f = f as Functional of (X + (Lin {v})) ;
A10: y |-- (W1,(Lin {y})) = [(0. W1),y] by A1, A2, Th15;
then A11: (y |-- (W1,(Lin {y}))) `1 = 0. X by MCART_1:7;
A12: f is additive
proof
let v1, v2 be Vector of (X + (Lin {v})); :: according to VECTSP_1:def_20 ::_thesis: f . (v1 + v2) = (f . v1) + (f . v2)
consider x1 being Vector of X, s1 being Element of K such that
A13: v1 |-- (W1,(Lin {y})) = [x1,(s1 * v)] by A1, A2, Th18;
A14: ( (v1 |-- (W1,(Lin {y}))) `1 = x1 & (v1 |-- (W1,(Lin {y}))) `2 = s1 * v ) by A13, MCART_1:7;
consider x2 being Vector of X, s2 being Element of K such that
A15: v2 |-- (W1,(Lin {y})) = [x2,(s2 * v)] by A1, A2, Th18;
A16: ( (v2 |-- (W1,(Lin {y}))) `1 = x2 & (v2 |-- (W1,(Lin {y}))) `2 = s2 * v ) by A15, MCART_1:7;
 (v1 + v2) |-- (W1,(Lin {y})) = [(x1 + x2),((s1 + s2) * v)] by A1, A2, A13, A15, Th19;
then  ( ((v1 + v2) |-- (W1,(Lin {y}))) `1 = x1 + x2 & ((v1 + v2) |-- (W1,(Lin {y}))) `2 = (s1 + s2) * v ) by MCART_1:7;
hence f . (v1 + v2) = (fi . (x1 + x2)) + ((s1 + s2) * r) by A7
.= (fi . (x1 + x2)) + ((s1 * r) + (s2 * r)) by VECTSP_1:def_3
.= ((fi . x1) + (fi . x2)) + ((s1 * r) + (s2 * r)) by VECTSP_1:def_20
.= (((fi . x1) + (fi . x2)) + (s1 * r)) + (s2 * r) by RLVECT_1:def_3
.= (((fi . x1) + (s1 * r)) + (fi . x2)) + (s2 * r) by RLVECT_1:def_3
.= ((fi . x1) + (s1 * r)) + ((fi . x2) + (s2 * r)) by RLVECT_1:def_3
.= (f . v1) + ((fi . x2) + (s2 * r)) by A7, A14
.= (f . v1) + (f . v2) by A7, A16 ;
::_thesis: verum
end;
 f is homogeneous
proof
let v0 be Vector of (X + (Lin {v})); :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds f . (b1 * v0) = b1 * (f . v0)
let t be Element of K; ::_thesis: f . (t * v0) = t * (f . v0)
consider x0 being Vector of X, s0 being Element of K such that
A17: v0 |-- (W1,(Lin {y})) = [x0,(s0 * v)] by A1, A2, Th18;
A18: ( (v0 |-- (W1,(Lin {y}))) `1 = x0 & (v0 |-- (W1,(Lin {y}))) `2 = s0 * v ) by A17, MCART_1:7;
 (t * v0) |-- (W1,(Lin {y})) = [(t * x0),((t * s0) * v)] by A1, A2, A17, Th20;
then  ( ((t * v0) |-- (W1,(Lin {y}))) `1 = t * x0 & ((t * v0) |-- (W1,(Lin {y}))) `2 = (t * s0) * v ) by MCART_1:7;
hence f . (t * v0) = (fi . (t * x0)) + ((t * s0) * r) by A7
.= (t * (fi . x0)) + ((t * s0) * r) by HAHNBAN1:def_8
.= (t * (fi . x0)) + (t * (s0 * r)) by GROUP_1:def_3
.= t * ((fi . x0) + (s0 * r)) by VECTSP_1:def_2
.= t * (f . v0) by A7, A18 ;
::_thesis: verum
end;
then reconsider f = f as linear-Functional of (X + (Lin {v})) by A12;
take  f ; ::_thesis: ( f | the carrier of X = fi & f . y = r )
A19: dom fi = the carrier of X by FUNCT_2:def_1;
 ( dom f = the carrier of (X + (Lin {v})) & X is Subspace of X + (Lin {v}) ) by FUNCT_2:def_1, VECTSP_5:7;
then  dom fi c= dom f by A19, VECTSP_4:def_2;
then  dom fi = (dom f) /\ the carrier of X by A19, XBOOLE_1:28;
hence  f | the carrier of X = fi by A8, FUNCT_1:46; ::_thesis: f . y = r
(y |-- (W1,(Lin {y}))) `2 = y by A10, MCART_1:7
.= (1_ K) * v by A1, VECTSP_1:def_17 ;
hence f . y = (fi . (0. X)) + ((1_ K) * r) by A7, A11
.= (0. K) + ((1_ K) * r) by HAHNBAN1:def_9
.= (0. K) + r by VECTSP_1:def_8
.= r by RLVECT_1:4 ;
::_thesis: verum
end;

registration
let K be non empty right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
clusterV1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive 0-preserving for Element of bool [: the carrier of V, the carrier of K:];
existence
 ex b1 being Functional of V st
( b1 is additive & b1 is 0-preserving )
proof
take  0Functional V ; ::_thesis: ( 0Functional V is additive & 0Functional V is 0-preserving )
thus  ( 0Functional V is additive & 0Functional V is 0-preserving ) ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
cluster Function-like quasi_total additive  ->  0-preserving for Element of bool [: the carrier of V, the carrier of K:];
coherence
 for b1 being Functional of V st b1 is additive holds
b1 is 0-preserving
proof
let f be Functional of V; ::_thesis: ( f is additive implies f is 0-preserving )
assume A1: f is additive ; ::_thesis: f is 0-preserving
f . (0. V) = f . ((0. V) + (0. V)) by RLVECT_1:def_4
.= (f . (0. V)) + (f . (0. V)) by A1, VECTSP_1:def_20 ;
hence  f . (0. V) = 0. K by RLVECT_1:9; :: according to HAHNBAN1:def_9 ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K;
cluster Function-like quasi_total homogeneous  ->  0-preserving for Element of bool [: the carrier of V, the carrier of K:];
coherence
 for b1 being Functional of V st b1 is homogeneous holds
b1 is 0-preserving
proof
let f be Functional of V; ::_thesis: ( f is homogeneous implies f is 0-preserving )
assume A1: f is homogeneous ; ::_thesis: f is 0-preserving
thus f . (0. V) = f . ((0. K) * (0. V)) by Th1
.= (0. K) * (f . (0. V)) by A1, HAHNBAN1:def_8
.= 0. K by VECTSP_1:7 ; :: according to HAHNBAN1:def_9 ::_thesis: verum
end;
end;

registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
cluster 0Functional V ->  constant ;
coherence
 0Functional V is constant
proof
let x, y be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not x in K48((0Functional V)) or not y in K48((0Functional V)) or (0Functional V) . x = (0Functional V) . y )
set f = 0Functional V;
assume  ( x in dom (0Functional V) & y in dom (0Functional V) ) ; ::_thesis: (0Functional V) . x = (0Functional V) . y
then reconsider v = x, w = y as Vector of V ;
thus (0Functional V) . x = (0Functional V) . v
.= 0. K by HAHNBAN1:14
.= (0Functional V) . w by HAHNBAN1:14
.= (0Functional V) . y ; ::_thesis: verum
end;
end;

registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
clusterV1() V4( the carrier of V) V5( the carrier of K) Function-like constant non empty V14( the carrier of V) quasi_total for Element of bool [: the carrier of V, the carrier of K:];
existence
 ex b1 being Functional of V st b1 is constant
proof
take  0Functional V ; ::_thesis: 0Functional V is constant
thus  0Functional V is constant ; ::_thesis: verum
end;
end;

definition
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
let f be 0-preserving Functional of V;
:: original: constant
redefine attrf is constant  means :Def7: :: VECTSP10:def 7
f = 0Functional V;
compatibility
 ( f is constant iff f = 0Functional V )
proof
A1: ( f . (0. V) = 0. K & the carrier of V = dom f ) by FUNCT_2:def_1, HAHNBAN1:def_9;
hereby  ::_thesis: ( f = 0Functional V implies f is constant )
assume A2: f is constant ; ::_thesis: f = 0Functional V
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._v_=_(0Functional_V)_._v
let v be Vector of V; ::_thesis: f . v = (0Functional V) . v
thus f . v = 0. K by A1, A2, FUNCT_1:def_10
.= (0Functional V) . v by HAHNBAN1:14 ; ::_thesis: verum
end;
hence  f = 0Functional V by FUNCT_2:63; ::_thesis: verum
end;
assume A3: f = 0Functional V ; ::_thesis: f is constant
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_f_holds_
f_._x_=_f_._y
let x, y be set ; ::_thesis: ( x in dom f & y in dom f implies f . x = f . y )
assume  ( x in dom f & y in dom f ) ; ::_thesis: f . x = f . y
then reconsider v = x, w = y as Vector of V ;
thus f . x = (0Functional V) . v by A3
.= 0. K by HAHNBAN1:14
.= (0Functional V) . w by HAHNBAN1:14
.= f . y by A3 ; ::_thesis: verum
end;
hence  f is constant by FUNCT_1:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines constant VECTSP10:def_7_:_
 for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V being non empty right_zeroed VectSpStr over K
for f being 0-preserving Functional of V holds
( f is constant iff f = 0Functional V );

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
clusterV1() V4( the carrier of V) V5( the carrier of K) Function-like constant non empty V14( the carrier of V) quasi_total additive 0-preserving for Element of bool [: the carrier of V, the carrier of K:];
existence
 ex b1 being Functional of V st
( b1 is constant & b1 is additive & b1 is 0-preserving )
proof
take  0Functional V ; ::_thesis: ( 0Functional V is constant & 0Functional V is additive & 0Functional V is 0-preserving )
thus  ( 0Functional V is constant & 0Functional V is additive & 0Functional V is 0-preserving ) ; ::_thesis: verum
end;
end;

registration
let K be Field;
let V be non trivial VectSp of K;
clusterV1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous for Element of bool [: the carrier of V, the carrier of K:];
existence
 ex b1 being Functional of V st
( b1 is additive & b1 is homogeneous & not b1 is constant & not b1 is trivial )
proof
consider v being Vector of V such that
A1: v <> 0. V by STRUCT_0:def_18;
set W = the Linear_Compl of Lin {v};
A2: V is_the_direct_sum_of the Linear_Compl of Lin {v}, Lin {v} by VECTSP_5:def_5;
then A3: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = the Linear_Compl of Lin {v} + (Lin {v}) by VECTSP_5:def_4;
then reconsider y = v as Vector of ( the Linear_Compl of Lin {v} + (Lin {v})) ;
A4: the Linear_Compl of Lin {v} /\ (Lin {v}) = (0). V by A2, VECTSP_5:def_4;
now__::_thesis:_not_v_in_the_Linear_Compl_of_Lin_{v}
 v in {v} by TARSKI:def_1;
then  v in Lin {v} by VECTSP_7:8;
then A5: v in the carrier of (Lin {v}) by STRUCT_0:def_5;
assume  v in the Linear_Compl of Lin {v} ; ::_thesis: contradiction
then  v in the carrier of the Linear_Compl of Lin {v} by STRUCT_0:def_5;
then  v in the carrier of the Linear_Compl of Lin {v} /\ the carrier of (Lin {v}) by A5, XBOOLE_0:def_4;
then  v in the carrier of ( the Linear_Compl of Lin {v} /\ (Lin {v})) by VECTSP_5:def_2;
then  v in {(0. V)} by A4, VECTSP_4:def_3;
hence  contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
then consider psi being linear-Functional of ( the Linear_Compl of Lin {v} + (Lin {v})) such that
 psi | the carrier of the Linear_Compl of Lin {v} = 0Functional the Linear_Compl of Lin {v} and
A6: psi . y = 1_ K by Th27;
reconsider f = psi as Functional of V by A3;
take  f ; ::_thesis: ( f is additive & f is homogeneous & not f is constant & not f is trivial )
thus  f is additive ::_thesis: ( f is homogeneous & not f is constant & not f is trivial )
proof
let v1, v2 be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: f . (v1 + v2) = (f . v1) + (f . v2)
reconsider w1 = v1, w2 = v2 as Vector of ( the Linear_Compl of Lin {v} + (Lin {v})) by A3;
 v1 + v2 = w1 + w2 by A3;
hence  f . (v1 + v2) = (f . v1) + (f . v2) by VECTSP_1:def_20; ::_thesis: verum
end;
thus  f is homogeneous ::_thesis: ( not f is constant & not f is trivial )
proof
let v1 be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds f . (b1 * v1) = b1 * (f . v1)
let a be Element of K; ::_thesis: f . (a * v1) = a * (f . v1)
reconsider w1 = v1 as Vector of ( the Linear_Compl of Lin {v} + (Lin {v})) by A3;
a * v1 = the lmult of ( the Linear_Compl of Lin {v} + (Lin {v})) . (a,w1) by A3
.= a * w1 ;
hence  f . (a * v1) = a * (f . v1) by HAHNBAN1:def_8; ::_thesis: verum
end;
then reconsider f1 = f as homogeneous Functional of V ;
thus  not f is constant ::_thesis: not f is trivial
proof
A7: ( the carrier of V = dom f & f1 . (0. V) = 0. K ) by FUNCT_2:def_1, HAHNBAN1:def_9;
assume  f is constant ; ::_thesis: contradiction
hence  contradiction by A6, A7, FUNCT_1:def_10; ::_thesis: verum
end;
thus  not f is trivial ::_thesis: verum
proof
set x = [v,(1_ K)];
set y = [(0. V),(0. K)];
A8: the carrier of V = dom f by FUNCT_2:def_1;
then A9: [v,(1_ K)] in f by A6, FUNCT_1:1;
 f1 . (0. V) = 0. K by HAHNBAN1:def_9;
then A10: [(0. V),(0. K)] in f by A8, FUNCT_1:1;
assume A11: f is trivial ; ::_thesis: contradiction
percases ( f = {} or ex z being set st f = {z} ) by A11, ZFMISC_1:131;
suppose f = {} ; ::_thesis: contradiction
hence  contradiction ; ::_thesis: verum
end;
suppose ex z being set st f = {z} ; ::_thesis: contradiction
then consider z being set  such that
A12: f = {z} ;
 ( z = [v,(1_ K)] & z = [(0. V),(0. K)] ) by A9, A10, A12, TARSKI:def_1;
hence  contradiction by XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
end;
end;

registration
let K be Field;
let V be non trivial VectSp of K;
cluster Function-like trivial quasi_total  ->  constant for Element of bool [: the carrier of V, the carrier of K:];
coherence
 for b1 being Functional of V st b1 is trivial holds
b1 is constant ;
end;

definition
let K be Field;
let V be non trivial VectSp of K;
let v be Vector of V;
let W be Linear_Compl of Lin {v};
assume A1: v <> 0. V ;
func coeffFunctional (v,W) ->  V8() non trivial linear-Functional of V means :Def8: :: VECTSP10:def 8
( it . v = 1_ K & it | the carrier of W = 0Functional W );
existence
 ex b1 being V8() non trivial linear-Functional of V st
( b1 . v = 1_ K & b1 | the carrier of W = 0Functional W )
proof
A2: V is_the_direct_sum_of W, Lin {v} by VECTSP_5:def_5;
then A3: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = W + (Lin {v}) by VECTSP_5:def_4;
then reconsider y = v as Vector of (W + (Lin {v})) ;
A4: W /\ (Lin {v}) = (0). V by A2, VECTSP_5:def_4;
now__::_thesis:_not_v_in_W
 v in {v} by TARSKI:def_1;
then  v in Lin {v} by VECTSP_7:8;
then A5: v in the carrier of (Lin {v}) by STRUCT_0:def_5;
assume  v in W ; ::_thesis: contradiction
then  v in the carrier of W by STRUCT_0:def_5;
then  v in the carrier of W /\ the carrier of (Lin {v}) by A5, XBOOLE_0:def_4;
then  v in the carrier of (W /\ (Lin {v})) by VECTSP_5:def_2;
then  v in {(0. V)} by A4, VECTSP_4:def_3;
hence  contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
then consider psi being linear-Functional of (W + (Lin {v})) such that
A6: psi | the carrier of W = 0Functional W and
A7: psi . y = 1_ K by Th27;
reconsider f = psi as Functional of V by A3;
A8: f is additive
proof
let v1, v2 be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: f . (v1 + v2) = (f . v1) + (f . v2)
reconsider w1 = v1, w2 = v2 as Vector of (W + (Lin {v})) by A3;
 v1 + v2 = w1 + w2 by A3;
hence  f . (v1 + v2) = (f . v1) + (f . v2) by VECTSP_1:def_20; ::_thesis: verum
end;
 f is homogeneous
proof
let v1 be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds f . (b1 * v1) = b1 * (f . v1)
let a be Element of K; ::_thesis: f . (a * v1) = a * (f . v1)
reconsider w1 = v1 as Vector of (W + (Lin {v})) by A3;
a * v1 = the lmult of (W + (Lin {v})) . (a,w1) by A3
.= a * w1 ;
hence  f . (a * v1) = a * (f . v1) by HAHNBAN1:def_8; ::_thesis: verum
end;
then reconsider f = f as linear-Functional of V by A8;
 f is V8()
proof
A9: ( the carrier of V = dom f & f . (0. V) = 0. K ) by FUNCT_2:def_1, HAHNBAN1:def_9;
assume  f is V8() ; ::_thesis: contradiction
hence  contradiction by A7, A9, FUNCT_1:def_10; ::_thesis: verum
end;
then reconsider f = f as V8() non trivial linear-Functional of V ;
take  f ; ::_thesis: ( f . v = 1_ K & f | the carrier of W = 0Functional W )
thus  ( f . v = 1_ K & f | the carrier of W = 0Functional W ) by A6, A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being V8() non trivial linear-Functional of V st b1 . v = 1_ K & b1 | the carrier of W = 0Functional W & b2 . v = 1_ K & b2 | the carrier of W = 0Functional W holds
b1 = b2
proof
let f1, f2 be V8() non trivial linear-Functional of V; ::_thesis: ( f1 . v = 1_ K & f1 | the carrier of W = 0Functional W & f2 . v = 1_ K & f2 | the carrier of W = 0Functional W implies f1 = f2 )
assume that
A10: f1 . v = 1_ K and
A11: f1 | the carrier of W = 0Functional W and
A12: f2 . v = 1_ K and
A13: f2 | the carrier of W = 0Functional W ; ::_thesis: f1 = f2
 V is_the_direct_sum_of W, Lin {v} by VECTSP_5:def_5;
then A14: VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = W + (Lin {v}) by VECTSP_5:def_4;
now__::_thesis:_for_w_being_Vector_of_V_holds_f1_._w_=_f2_._w
let w be Vector of V; ::_thesis: f1 . w = f2 . w
 w in W + (Lin {v}) by A14, STRUCT_0:def_5;
then consider v1, v2 being Vector of V such that
A15: v1 in W and
A16: v2 in Lin {v} and
A17: w = v1 + v2 by VECTSP_5:1;
consider a being Element of K such that
A18: v2 = a * v by A16, Th3;
A19: v1 in the carrier of W by A15, STRUCT_0:def_5;
then A20: f1 . v1 = (f2 | the carrier of W) . v1 by A11, A13, FUNCT_1:49
.= f2 . v1 by A19, FUNCT_1:49 ;
thus f1 . w = (f1 . v1) + (f1 . (a * v)) by A17, A18, VECTSP_1:def_20
.= (f1 . v1) + (a * (f1 . v)) by HAHNBAN1:def_8
.= (f1 . v1) + (f2 . (a * v)) by A10, A12, HAHNBAN1:def_8
.= f2 . w by A17, A18, A20, VECTSP_1:def_20 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines coeffFunctional VECTSP10:def_8_:_
 for K being Field
for V being non trivial VectSp of K
for v being Vector of V
for W being Linear_Compl of Lin {v} st v <> 0. V holds
for b5 being V8() non trivial linear-Functional of V holds
( b5 = coeffFunctional (v,W) iff ( b5 . v = 1_ K & b5 | the carrier of W = 0Functional W ) );

theorem Th28: :: VECTSP10:28
for K being Field
for V being non trivial VectSp of K
for f being V8() 0-preserving Functional of V ex v being Vector of V st
( v <> 0. V & f . v <> 0. K )
proof
let K be Field; ::_thesis: for V being non trivial VectSp of K
for f being V8() 0-preserving Functional of V ex v being Vector of V st
( v <> 0. V & f . v <> 0. K )
let V be non trivial VectSp of K; ::_thesis: for f being V8() 0-preserving Functional of V ex v being Vector of V st
( v <> 0. V & f . v <> 0. K )
let f be V8() 0-preserving Functional of V; ::_thesis: ex v being Vector of V st
( v <> 0. V & f . v <> 0. K )
A1: f . (0. V) = 0. K by HAHNBAN1:def_9;
assume A2: for v being Vector of V st v <> 0. V holds
f . v = 0. K ; ::_thesis: contradiction
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_f_holds_
f_._x_=_f_._y
let x, y be set ; ::_thesis: ( x in dom f & y in dom f implies f . x = f . y )
assume  ( x in dom f & y in dom f ) ; ::_thesis: f . x = f . y
then reconsider v = x, w = y as Vector of V ;
thus f . x = f . v
.= 0. K by A2, A1
.= f . w by A2, A1
.= f . y ; ::_thesis: verum
end;
hence  contradiction by FUNCT_1:def_10; ::_thesis: verum
end;

theorem Th29: :: VECTSP10:29
for K being Field
for V being non trivial VectSp of K
for v being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
proof
let K be Field; ::_thesis: for V being non trivial VectSp of K
for v being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
let V be non trivial VectSp of K; ::_thesis: for v being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
let v be Vector of V; ::_thesis: for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
let a be Scalar of ; ::_thesis: for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
let W be Linear_Compl of Lin {v}; ::_thesis: ( v <> 0. V implies (coeffFunctional (v,W)) . (a * v) = a )
assume A1: v <> 0. V ; ::_thesis: (coeffFunctional (v,W)) . (a * v) = a
set cf = coeffFunctional (v,W);
thus (coeffFunctional (v,W)) . (a * v) = a * ((coeffFunctional (v,W)) . v) by HAHNBAN1:def_8
.= a * (1_ K) by A1, Def8
.= a by VECTSP_1:def_8 ; ::_thesis: verum
end;

theorem Th30: :: VECTSP10:30
for K being Field
for V being non trivial VectSp of K
for v, w being Vector of V
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . w = 0. K
proof
let K be Field; ::_thesis: for V being non trivial VectSp of K
for v, w being Vector of V
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . w = 0. K
let V be non trivial VectSp of K; ::_thesis: for v, w being Vector of V
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . w = 0. K
let v, w be Vector of V; ::_thesis: for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . w = 0. K
let W be Linear_Compl of Lin {v}; ::_thesis: ( v <> 0. V & w in W implies (coeffFunctional (v,W)) . w = 0. K )
assume that
A1: v <> 0. V and
A2: w in W ; ::_thesis: (coeffFunctional (v,W)) . w = 0. K
set cf = coeffFunctional (v,W);
set cw = the carrier of W;
reconsider s = w as Vector of W by A2, STRUCT_0:def_5;
 w in the carrier of W by A2, STRUCT_0:def_5;
hence (coeffFunctional (v,W)) . w = ((coeffFunctional (v,W)) | the carrier of W) . w by FUNCT_1:49
.= (0Functional W) . s by A1, Def8
.= 0. K by HAHNBAN1:14 ;
::_thesis: verum
end;

theorem :: VECTSP10:31
for K being Field
for V being non trivial VectSp of K
for v, w being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . ((a * v) + w) = a
proof
let K be Field; ::_thesis: for V being non trivial VectSp of K
for v, w being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . ((a * v) + w) = a
let V be non trivial VectSp of K; ::_thesis: for v, w being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . ((a * v) + w) = a
let v, w be Vector of V; ::_thesis: for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . ((a * v) + w) = a
let a be Scalar of ; ::_thesis: for W being Linear_Compl of Lin {v} st v <> 0. V & w in W holds
(coeffFunctional (v,W)) . ((a * v) + w) = a
let W be Linear_Compl of Lin {v}; ::_thesis: ( v <> 0. V & w in W implies (coeffFunctional (v,W)) . ((a * v) + w) = a )
assume that
A1: v <> 0. V and
A2: w in W ; ::_thesis: (coeffFunctional (v,W)) . ((a * v) + w) = a
set cf = coeffFunctional (v,W);
thus (coeffFunctional (v,W)) . ((a * v) + w) = ((coeffFunctional (v,W)) . (a * v)) + ((coeffFunctional (v,W)) . w) by VECTSP_1:def_20
.= ((coeffFunctional (v,W)) . (a * v)) + (0. K) by A1, A2, Th30
.= (coeffFunctional (v,W)) . (a * v) by RLVECT_1:def_4
.= a by A1, Th29 ; ::_thesis: verum
end;

theorem :: VECTSP10:32
for K being non empty addLoopStr
for V being non empty VectSpStr over K
for f, g being Functional of V
for v being Vector of V holds (f - g) . v = (f . v) - (g . v)
proof
let K be non empty addLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for f, g being Functional of V
for v being Vector of V holds (f - g) . v = (f . v) - (g . v)
let V be non empty VectSpStr over K; ::_thesis: for f, g being Functional of V
for v being Vector of V holds (f - g) . v = (f . v) - (g . v)
let f, g be Functional of V; ::_thesis: for v being Vector of V holds (f - g) . v = (f . v) - (g . v)
let v be Vector of V; ::_thesis: (f - g) . v = (f . v) - (g . v)
thus (f - g) . v = (f . v) + ((- g) . v) by HAHNBAN1:def_3
.= (f . v) - (g . v) by HAHNBAN1:def_4 ; ::_thesis: verum
end;

registration
let K be Field;
let V be non trivial VectSp of K;
clusterV *'  ->  non trivial ;
coherence
 not V *' is trivial
proof
set g = the V8() linear-Functional of V;
A1: the V8() linear-Functional of V <> 0Functional V ;
reconsider g = the V8() linear-Functional of V as Element of (V *') by HAHNBAN1:def_10;
assume  V *' is trivial ; ::_thesis: contradiction
then  g = 0. (V *') by STRUCT_0:def_18;
hence  contradiction by A1, HAHNBAN1:def_10; ::_thesis: verum
end;
end;

begin

definition
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
let f be Functional of V;
func ker f ->  Subset of V equals :: VECTSP10:def 9
 {  v where v is Vector of V : f . v = 0. K  }  ;
coherence
  {  v where v is Vector of V : f . v = 0. K  }  is Subset of V
proof
set A =  {  v where v is Vector of V : f . v = 0. K  }  ;
  {  v where v is Vector of V : f . v = 0. K  }  c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  v where v is Vector of V : f . v = 0. K  }  or x in the carrier of V )
assume  x in  {  v where v is Vector of V : f . v = 0. K  }  ; ::_thesis: x in the carrier of V
then  ex v being Vector of V st
( v = x & f . v = 0. K ) ;
hence  x in the carrier of V ; ::_thesis: verum
end;
hence   {  v where v is Vector of V : f . v = 0. K  }  is Subset of V ; ::_thesis: verum
end;
end;

:: deftheorem  defines ker VECTSP10:def_9_:_
 for K being non empty ZeroStr
for V being non empty VectSpStr over K
for f being Functional of V holds ker f =  {  v where v is Vector of V : f . v = 0. K  }  ;

registration
let K be non empty right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
let f be 0-preserving Functional of V;
cluster ker f ->  non empty ;
coherence
 not ker f is empty
proof
 f . (0. V) = 0. K by HAHNBAN1:def_9;
then  0. V in ker f ;
hence  not ker f is empty ; ::_thesis: verum
end;
end;

theorem Th33: :: VECTSP10:33
for K being non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for f being linear-Functional of V holds ker f is linearly-closed
proof
let F be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for f being linear-Functional of V holds ker f is linearly-closed
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F; ::_thesis: for f being linear-Functional of V holds ker f is linearly-closed
let f be linear-Functional of V; ::_thesis: ker f is linearly-closed
set V1 = ker f;
thus  for v, u being Vector of V st v in ker f & u in ker f holds
v + u in ker f :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of F
for b2 being Element of the carrier of V holds
( not b2 in ker f or b1 * b2 in ker f )
proof
let v, u be Vector of V; ::_thesis: ( v in ker f & u in ker f implies v + u in ker f )
assume  ( v in ker f & u in ker f ) ; ::_thesis: v + u in ker f
then  ( ex a being Vector of V st
( a = v & f . a = 0. F ) & ex b being Vector of V st
( b = u & f . b = 0. F ) ) ;
then f . (v + u) = (0. F) + (0. F) by VECTSP_1:def_20
.= 0. F by RLVECT_1:4 ;
hence  v + u in ker f ; ::_thesis: verum
end;
let a be Element of F; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in ker f or a * b1 in ker f )
let v be Vector of V; ::_thesis: ( not v in ker f or a * v in ker f )
assume  v in ker f ; ::_thesis: a * v in ker f
then  ex w being Vector of V st
( w = v & f . w = 0. F ) ;
then f . (a * v) = a * (0. F) by HAHNBAN1:def_8
.= 0. F by VECTSP_1:6 ;
hence  a * v in ker f ; ::_thesis: verum
end;

definition
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
let f be Functional of V;
attrf is degenerated  means :Def10: :: VECTSP10:def 10
 ker f <> {(0. V)};
end;

:: deftheorem Def10 defines degenerated VECTSP10:def_10_:_
 for K being non empty ZeroStr
for V being non empty VectSpStr over K
for f being Functional of V holds
( f is degenerated iff ker f <> {(0. V)} );

registration
let K be non empty non degenerated doubleLoopStr ;
let V be non trivial VectSpStr over K;
cluster Function-like quasi_total 0-preserving non degenerated  ->  non constant for Element of bool [: the carrier of V, the carrier of K:];
coherence
 for b1 being Functional of V st not b1 is degenerated & b1 is 0-preserving holds
not b1 is constant
proof
let f be Functional of V; ::_thesis: ( not f is degenerated & f is 0-preserving implies not f is constant )
assume that
A1: not f is degenerated and
A2: f is 0-preserving and
A3: f is constant ; ::_thesis: contradiction
A4: f . (0. V) = 0. K by A2, HAHNBAN1:def_9;
A5: now__::_thesis:_ex_v_being_Vector_of_V_st_
(_v_<>_0._V_&_not_f_._v_=_0._K_)
assume A6: for v being Vector of V st v <> 0. V holds
f . v = 0. K ; ::_thesis: contradiction
 the carrier of V c= ker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of V or x in ker f )
assume  x in the carrier of V ; ::_thesis: x in ker f
then reconsider v = x as Vector of V ;
percases ( v = 0. V or v <> 0. V ) ;
suppose v = 0. V ; ::_thesis: x in ker f
hence  x in ker f by A4; ::_thesis: verum
end;
suppose v <> 0. V ; ::_thesis: x in ker f
then  f . v = 0. K by A6;
hence  x in ker f ; ::_thesis: verum
end;
end;
end;
then  the carrier of V = ker f by XBOOLE_0:def_10
.= {(0. V)} by A1, Def10 ;
hence  contradiction ; ::_thesis: verum
end;
 dom f = the carrier of V by FUNCT_2:def_1;
hence  contradiction by A3, A4, A5, FUNCT_1:def_10; ::_thesis: verum
end;
end;

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let f be linear-Functional of V;
func Ker f ->  non empty strict Subspace of V means :Def11: :: VECTSP10:def 11
 the carrier of it = ker f;
existence
 ex b1 being non empty strict Subspace of V st the carrier of b1 = ker f by Th33, VECTSP_4:34;
uniqueness
 for b1, b2 being non empty strict Subspace of V st the carrier of b1 = ker f & the carrier of b2 = ker f holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def11 defines Ker VECTSP10:def_11_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for f being linear-Functional of V
for b4 being non empty strict Subspace of V holds
( b4 = Ker f iff the carrier of b4 = ker f );

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be Subspace of V;
let f be additive Functional of V;
assume A1: the carrier of W c= ker f ;
func QFunctional (f,W) ->  additive Functional of (VectQuot (V,W)) means :Def12: :: VECTSP10:def 12
 for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
it . A = f . a;
existence
 ex b1 being additive Functional of (VectQuot (V,W)) st
for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b1 . A = f . a
proof
defpred S1[ set , set ] means  for a being Vector of V st $1 = a + W holds
$2 = f . a;
set aC = addCoset (V,W);
set C = CosetSet (V,W);
set vq = VectQuot (V,W);
A2: now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,W))_ex_y_being_Element_of_the_carrier_of_K_st_S1[A,y]
let A be Vector of (VectQuot (V,W)); ::_thesis: ex y being Element of the carrier of K st S1[A,y]
consider a being Vector of V such that
A3: A = a + W by Th22;
take y = f . a; ::_thesis: S1[A,y]
thus  S1[A,y] ::_thesis: verum
proof
let a1 be Vector of V; ::_thesis: ( A = a1 + W implies y = f . a1 )
assume  A = a1 + W ; ::_thesis: y = f . a1
then  a in a1 + W by A3, VECTSP_4:44;
then consider w being Vector of V such that
A4: w in W and
A5: a = a1 + w by VECTSP_4:42;
 w in the carrier of W by A4, STRUCT_0:def_5;
then  w in ker f by A1;
then A6: ex aa being Vector of V st
( aa = w & f . aa = 0. K ) ;
thus y = (f . a1) + (f . w) by A5, VECTSP_1:def_20
.= f . a1 by A6, RLVECT_1:def_4 ; ::_thesis: verum
end;
end;
consider ff being Function of the carrier of (VectQuot (V,W)), the carrier of K such that
A7: for A being Vector of (VectQuot (V,W)) holds S1[A,ff . A] from FUNCT_2:sch_3(A2);
reconsider ff = ff as Functional of (VectQuot (V,W)) ;
A8: CosetSet (V,W) = the carrier of (VectQuot (V,W)) by Def6;
now__::_thesis:_for_A,_B_being_Vector_of_(VectQuot_(V,W))_holds_ff_._(A_+_B)_=_(ff_._A)_+_(ff_._B)
A9: the addF of (VectQuot (V,W)) = addCoset (V,W) by Def6;
let A, B be Vector of (VectQuot (V,W)); ::_thesis: ff . (A + B) = (ff . A) + (ff . B)
consider a being Vector of V such that
A10: A = a + W by Th22;
consider b being Vector of V such that
A11: B = b + W by Th22;
 (addCoset (V,W)) . (A,B) = (a + b) + W by A8, A10, A11, Def3;
hence ff . (A + B) = f . (a + b) by A7, A9
.= (f . a) + (f . b) by VECTSP_1:def_20
.= (ff . A) + (f . b) by A7, A10
.= (ff . A) + (ff . B) by A7, A11 ;
::_thesis: verum
end;
then reconsider ff = ff as additive Functional of (VectQuot (V,W)) by VECTSP_1:def_20;
take  ff ; ::_thesis: for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
ff . A = f . a
thus  for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
ff . A = f . a by A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being additive Functional of (VectQuot (V,W)) st ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b1 . A = f . a ) & ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b2 . A = f . a ) holds
b1 = b2
proof
set vq = VectQuot (V,W);
let f1, f2 be additive Functional of (VectQuot (V,W)); ::_thesis: ( ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
f1 . A = f . a ) & ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
f2 . A = f . a ) implies f1 = f2 )
assume that
A12: for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
f1 . A = f . a and
A13: for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
f2 . A = f . a ; ::_thesis: f1 = f2
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,W))_holds_f1_._A_=_f2_._A
let A be Vector of (VectQuot (V,W)); ::_thesis: f1 . A = f2 . A
consider a being Vector of V such that
A14: A = a + W by Th22;
thus f1 . A = f . a by A12, A14
.= f2 . A by A13, A14 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines QFunctional VECTSP10:def_12_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for f being additive Functional of V st the carrier of W c= ker f holds
for b5 being additive Functional of (VectQuot (V,W)) holds
( b5 = QFunctional (f,W) iff for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b5 . A = f . a );

theorem Th34: :: VECTSP10:34
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional (f,W) is homogeneous
proof
let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of F
for W being Subspace of V
for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional (f,W) is homogeneous
let V be VectSp of F; ::_thesis: for W being Subspace of V
for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional (f,W) is homogeneous
let W be Subspace of V; ::_thesis: for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional (f,W) is homogeneous
let f be linear-Functional of V; ::_thesis: ( the carrier of W c= ker f implies QFunctional (f,W) is homogeneous )
set qf = QFunctional (f,W);
set vq = VectQuot (V,W);
assume A1: the carrier of W c= ker f ; ::_thesis: QFunctional (f,W) is homogeneous
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,W))
for_r_being_Scalar_of_holds_(QFunctional_(f,W))_._(r_*_A)_=_r_*_((QFunctional_(f,W))_._A)
set C = CosetSet (V,W);
let A be Vector of (VectQuot (V,W)); ::_thesis: for r being Scalar of holds (QFunctional (f,W)) . (r * A) = r * ((QFunctional (f,W)) . A)
let r be Scalar of ; ::_thesis: (QFunctional (f,W)) . (r * A) = r * ((QFunctional (f,W)) . A)
A2: CosetSet (V,W) = the carrier of (VectQuot (V,W)) by Def6;
then  A in CosetSet (V,W) ;
then consider aa being Coset of W such that
A3: A = aa ;
consider a being Vector of V such that
A4: aa = a + W by VECTSP_4:def_6;
r * A = the lmult of (VectQuot (V,W)) . (r,A)
.= (lmultCoset (V,W)) . (r,A) by Def6
.= (r * a) + W by A2, A3, A4, Def5 ;
hence (QFunctional (f,W)) . (r * A) = f . (r * a) by A1, Def12
.= r * (f . a) by HAHNBAN1:def_8
.= r * ((QFunctional (f,W)) . A) by A1, A3, A4, Def12 ;
::_thesis: verum
end;
hence  QFunctional (f,W) is homogeneous by HAHNBAN1:def_8; ::_thesis: verum
end;

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let f be linear-Functional of V;
func CQFunctional f ->  linear-Functional of (VectQuot (V,(Ker f))) equals :: VECTSP10:def 13
 QFunctional (f,(Ker f));
correctness
coherence
QFunctional (f,(Ker f)) is linear-Functional of (VectQuot (V,(Ker f)));
proof
 the carrier of (Ker f) = ker f by Def11;
hence  QFunctional (f,(Ker f)) is linear-Functional of (VectQuot (V,(Ker f))) by Th34; ::_thesis: verum
end;
end;

:: deftheorem  defines CQFunctional VECTSP10:def_13_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for f being linear-Functional of V holds CQFunctional f = QFunctional (f,(Ker f));

theorem Th35: :: VECTSP10:35
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for f being linear-Functional of V
for A being Vector of (VectQuot (V,(Ker f)))
for v being Vector of V st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for f being linear-Functional of V
for A being Vector of (VectQuot (V,(Ker f)))
for v being Vector of V st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let V be VectSp of K; ::_thesis: for f being linear-Functional of V
for A being Vector of (VectQuot (V,(Ker f)))
for v being Vector of V st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let f be linear-Functional of V; ::_thesis: for A being Vector of (VectQuot (V,(Ker f)))
for v being Vector of V st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let A be Vector of (VectQuot (V,(Ker f))); ::_thesis: for v being Vector of V st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let v be Vector of V; ::_thesis: ( A = v + (Ker f) implies (CQFunctional f) . A = f . v )
assume A1: A = v + (Ker f) ; ::_thesis: (CQFunctional f) . A = f . v
 the carrier of (Ker f) = ker f by Def11;
hence  (CQFunctional f) . A = f . v by A1, Def12; ::_thesis: verum
end;

registration
let K be Field;
let V be non trivial VectSp of K;
let f be V8() linear-Functional of V;
cluster CQFunctional f -> V8() ;
coherence
 not CQFunctional f is constant
proof
set W = Ker f;
set qf = CQFunctional f;
set qv = VectQuot (V,(Ker f));
consider v being Vector of V such that
 v <> 0. V and
A1: f . v <> 0. K by Th28;
reconsider cv = v + (Ker f) as Vector of (VectQuot (V,(Ker f))) by Th23;
assume  CQFunctional f is V8() ; ::_thesis: contradiction
then  CQFunctional f = 0Functional (VectQuot (V,(Ker f))) by Def7;
then  0. K = (CQFunctional f) . cv by HAHNBAN1:14
.= f . v by Th35 ;
hence  contradiction by A1; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let f be linear-Functional of V;
cluster CQFunctional f ->  non degenerated ;
coherence
 not CQFunctional f is degenerated
proof
set qf = CQFunctional f;
set W = Ker f;
set qV = VectQuot (V,(Ker f));
A1: the carrier of (Ker f) = ker f by Def11;
A2: the carrier of (VectQuot (V,(Ker f))) = CosetSet (V,(Ker f)) by Def6;
thus  ker (CQFunctional f) c= {(0. (VectQuot (V,(Ker f))))} :: according to XBOOLE_0:def_10,VECTSP10:def_10 ::_thesis: {(0. (VectQuot (V,(Ker f))))} c= ker (CQFunctional f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ker (CQFunctional f) or x in {(0. (VectQuot (V,(Ker f))))} )
assume  x in ker (CQFunctional f) ; ::_thesis: x in {(0. (VectQuot (V,(Ker f))))}
then consider w being Vector of (VectQuot (V,(Ker f))) such that
A3: x = w and
A4: (CQFunctional f) . w = 0. K ;
 w in CosetSet (V,(Ker f)) by A2;
then consider A being Coset of Ker f such that
A5: w = A ;
consider v being Vector of V such that
A6: A = v + (Ker f) by VECTSP_4:def_6;
 f . v = 0. K by A1, A4, A5, A6, Def12;
then  v in ker f ;
then  v in Ker f by A1, STRUCT_0:def_5;
then w = zeroCoset (V,(Ker f)) by A5, A6, VECTSP_4:49
.= 0. (VectQuot (V,(Ker f))) by Th21 ;
hence  x in {(0. (VectQuot (V,(Ker f))))} by A3, TARSKI:def_1; ::_thesis: verum
end;
thus  {(0. (VectQuot (V,(Ker f))))} c= ker (CQFunctional f) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. (VectQuot (V,(Ker f))))} or x in ker (CQFunctional f) )
assume  x in {(0. (VectQuot (V,(Ker f))))} ; ::_thesis: x in ker (CQFunctional f)
then A7: x = 0. (VectQuot (V,(Ker f))) by TARSKI:def_1;
 (CQFunctional f) . (0. (VectQuot (V,(Ker f)))) = 0. K by HAHNBAN1:def_9;
hence  x in ker (CQFunctional f) by A7; ::_thesis: verum
end;
end;
end;