set S = LC_RLSpace V;
A1: now :: thesis: for v, u being VECTOR of ()
for K, L being Linear_Combination of V st v = K & u = L holds
v + u = K + L
let v, u be VECTOR of (); :: thesis: for K, L being Linear_Combination of V st v = K & u = L holds
v + u = K + L

let K, L be Linear_Combination of V; :: thesis: ( v = K & u = L implies v + u = K + L )
A2: ( @ (@ K) = K & @ (@ L) = L ) ;
assume ( v = K & u = L ) ; :: thesis: v + u = K + L
hence v + u = K + L by ; :: thesis: verum
end;
thus LC_RLSpace V is Abelian :: thesis:
proof
let u, v be Element of (); :: according to RLVECT_1:def 2 :: thesis: u + v = v + u
reconsider K = u, L = v as Linear_Combination of V by Def14;
thus u + v = L + K by A1
.= v + u by A1 ; :: thesis: verum
end;
thus LC_RLSpace V is add-associative :: thesis:
proof
let u, v, w be Element of (); :: according to RLVECT_1:def 3 :: thesis: (u + v) + w = u + (v + w)
reconsider L = u, K = v, M = w as Linear_Combination of V by Def14;
A3: v + w = K + M by A1;
u + v = L + K by A1;
hence (u + v) + w = (L + K) + M by A1
.= L + (K + M) by Th40
.= u + (v + w) by A1, A3 ;
:: thesis: verum
end;
thus LC_RLSpace V is right_zeroed :: thesis:
proof
let v be Element of (); :: according to RLVECT_1:def 4 :: thesis: v + (0. ()) = v
reconsider K = v as Linear_Combination of V by Def14;
thus v + (0. ()) = K + () by A1
.= v by Th41 ; :: thesis: verum
end;
thus LC_RLSpace V is right_complementable :: thesis:
proof
let v be Element of (); :: according to ALGSTR_0:def 16 :: thesis:
reconsider K = v as Linear_Combination of V by Def14;
- K in the carrier of () by Def14;
then - K in LC_RLSpace V ;
then - K = vector ((),(- K)) by Def1;
then v + (vector ((),(- K))) = K - K by A1
.= 0. () by Th57 ;
hence ex w being VECTOR of () st v + w = 0. () ; :: according to ALGSTR_0:def 11 :: thesis: verum
end;
A4: now :: thesis: for v being VECTOR of ()
for L being Linear_Combination of V
for a being Real st v = L holds
a * v = a * L
let v be VECTOR of (); :: thesis: for L being Linear_Combination of V
for a being Real st v = L holds
a * v = a * L

let L be Linear_Combination of V; :: thesis: for a being Real st v = L holds
a * v = a * L

let a be Real; :: thesis: ( v = L implies a * v = a * L )
A5: @ (@ L) = L ;
assume v = L ; :: thesis: a * v = a * L
hence a * v = a * L by ; :: thesis: verum
end;
thus for a being Real
for v, w being VECTOR of () holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def 5 :: thesis:
proof
let a be Real; :: thesis: for v, w being VECTOR of () holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of (); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider K = v, M = w as Linear_Combination of V by Def14;
reconsider a = a as Real ;
A6: ( a * v = a * K & a * w = a * M ) by A4;
v + w = K + M by A1;
then a * (v + w) = a * (K + M) by A4
.= (a * K) + (a * M) by Th46
.= (a * v) + (a * w) by A1, A6 ;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum
end;
thus for a, b being Real
for v being VECTOR of () holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def 6 :: thesis:
proof
let a, b be Real; :: thesis: for v being VECTOR of () holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of (); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider K = v as Linear_Combination of V by Def14;
reconsider a = a, b = b as Real ;
A7: ( a * v = a * K & b * v = b * K ) by A4;
(a + b) * v = (a + b) * K by A4
.= (a * K) + (b * K) by Th45
.= (a * v) + (b * v) by A1, A7 ;
hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum
end;
thus for a, b being Real
for v being VECTOR of () holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def 7 :: thesis:
proof
let a, b be Real; :: thesis: for v being VECTOR of () holds (a * b) * v = a * (b * v)
let v be VECTOR of (); :: thesis: (a * b) * v = a * (b * v)
reconsider K = v as Linear_Combination of V by Def14;
reconsider a = a, b = b as Real ;
A8: b * v = b * K by A4;
(a * b) * v = (a * b) * K by A4
.= a * (b * K) by Th47
.= a * (b * v) by A4, A8 ;
hence (a * b) * v = a * (b * v) ; :: thesis: verum
end;
let v be VECTOR of (); :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
reconsider K = v as Linear_Combination of V by Def14;
thus 1 * v = 1 * K by A4
.= v by Th48 ; :: thesis: verum