set S = LC_RLSpace V;

for v, w being VECTOR of (LC_RLSpace V) holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def 5 :: thesis: ( LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )

for v being VECTOR of (LC_RLSpace V) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def 6 :: thesis: ( LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )

for v being VECTOR of (LC_RLSpace V) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def 7 :: thesis: LC_RLSpace V is scalar-unital

reconsider K = v as Linear_Combination of V by Def14;

thus 1 * v = 1 * K by A4

.= v by Th48 ; :: thesis: verum

A1: now :: thesis: for v, u being VECTOR of (LC_RLSpace V)

for K, L being Linear_Combination of V st v = K & u = L holds

v + u = K + L

thus
LC_RLSpace V is Abelian
:: thesis: ( LC_RLSpace V is add-associative & LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )for K, L being Linear_Combination of V st v = K & u = L holds

v + u = K + L

let v, u be VECTOR of (LC_RLSpace V); :: 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 A2, Def17; :: thesis: verum

end;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 A2, Def17; :: thesis: verum

proof

thus
LC_RLSpace V is add-associative
:: thesis: ( LC_RLSpace V is right_zeroed & LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
let u, v be Element of (LC_RLSpace V); :: 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;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

proof

thus
LC_RLSpace V is right_zeroed
:: thesis: ( LC_RLSpace V is right_complementable & LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
let u, v, w be Element of (LC_RLSpace V); :: 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;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

proof

thus
LC_RLSpace V is right_complementable
:: thesis: ( LC_RLSpace V is vector-distributive & LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )
let v be Element of (LC_RLSpace V); :: according to RLVECT_1:def 4 :: thesis: v + (0. (LC_RLSpace V)) = v

reconsider K = v as Linear_Combination of V by Def14;

thus v + (0. (LC_RLSpace V)) = K + (ZeroLC V) by A1

.= v by Th41 ; :: thesis: verum

end;reconsider K = v as Linear_Combination of V by Def14;

thus v + (0. (LC_RLSpace V)) = K + (ZeroLC V) by A1

.= v by Th41 ; :: thesis: verum

proof

let v be Element of (LC_RLSpace V); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

reconsider K = v as Linear_Combination of V by Def14;

- K in the carrier of (LC_RLSpace V) by Def14;

then - K in LC_RLSpace V ;

then - K = vector ((LC_RLSpace V),(- K)) by Def1;

then v + (vector ((LC_RLSpace V),(- K))) = K - K by A1

.= 0. (LC_RLSpace V) by Th57 ;

hence ex w being VECTOR of (LC_RLSpace V) st v + w = 0. (LC_RLSpace V) ; :: according to ALGSTR_0:def 11 :: thesis: verum

end;reconsider K = v as Linear_Combination of V by Def14;

- K in the carrier of (LC_RLSpace V) by Def14;

then - K in LC_RLSpace V ;

then - K = vector ((LC_RLSpace V),(- K)) by Def1;

then v + (vector ((LC_RLSpace V),(- K))) = K - K by A1

.= 0. (LC_RLSpace V) by Th57 ;

hence ex w being VECTOR of (LC_RLSpace V) st v + w = 0. (LC_RLSpace V) ; :: according to ALGSTR_0:def 11 :: thesis: verum

A4: now :: thesis: for v being VECTOR of (LC_RLSpace V)

for L being Linear_Combination of V

for a being Real st v = L holds

a * v = a * L

thus
for a being Realfor L being Linear_Combination of V

for a being Real st v = L holds

a * v = a * L

let v be VECTOR of (LC_RLSpace V); :: 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 A5, Def18; :: thesis: verum

end;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 A5, Def18; :: thesis: verum

for v, w being VECTOR of (LC_RLSpace V) holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def 5 :: thesis: ( LC_RLSpace V is scalar-distributive & LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )

proof

thus
for a, b being Real
let a be Real; :: thesis: for v, w being VECTOR of (LC_RLSpace V) holds a * (v + w) = (a * v) + (a * w)

let v, w be VECTOR of (LC_RLSpace V); :: 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;let v, w be VECTOR of (LC_RLSpace V); :: 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

for v being VECTOR of (LC_RLSpace V) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def 6 :: thesis: ( LC_RLSpace V is scalar-associative & LC_RLSpace V is scalar-unital )

proof

thus
for a, b being Real
let a, b be Real; :: thesis: for v being VECTOR of (LC_RLSpace V) holds (a + b) * v = (a * v) + (b * v)

let v be VECTOR of (LC_RLSpace V); :: 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;let v be VECTOR of (LC_RLSpace V); :: 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

for v being VECTOR of (LC_RLSpace V) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def 7 :: thesis: LC_RLSpace V is scalar-unital

proof

let v be VECTOR of (LC_RLSpace V); :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
let a, b be Real; :: thesis: for v being VECTOR of (LC_RLSpace V) holds (a * b) * v = a * (b * v)

let v be VECTOR of (LC_RLSpace V); :: 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 (LC_RLSpace V); :: 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

reconsider K = v as Linear_Combination of V by Def14;

thus 1 * v = 1 * K by A4

.= v by Th48 ; :: thesis: verum