set S = LC_Z_Module 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_Z_Module 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 Def29;
thus u + v = K + L by A1
.= L + K
.= v + u by A1 ; :: thesis: verum
end;
thus LC_Z_Module 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 Def29;
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 Th28
.= u + (v + w) by A1, A3 ;
:: thesis: verum
end;
thus LC_Z_Module 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 Def29;
thus v + (0. ()) = K + () by A1
.= v ; :: thesis: verum
end;
thus LC_Z_Module 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 Def29;
- K in the carrier of () by Def29;
then - K in LC_Z_Module V ;
then - K = vector ((),(- K)) by RLVECT_2:def 1;
then v + (vector ((),(- K))) = K - K by A1
.= 0. () by Th42 ;
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 Element of R st v = L holds
a * v = a * L
let v be Vector of (); :: thesis: for L being Linear_Combination of V
for a being Element of R st v = L holds
a * v = a * L

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

let a be Element of R; :: 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 LC_Z_Module V is vector-distributive :: thesis:
proof
let a be Element of R; :: according to VECTSP_1:def 13 :: thesis: for b1, b2 being Element of the carrier of () holds a * (b1 + b2) = (a * b1) + (a * b2)
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 Def29;
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 Th33
.= (a * v) + (a * w) by A1, A6 ;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum
end;
thus LC_Z_Module V is scalar-distributive :: thesis:
proof
let a, b be Element of R; :: according to VECTSP_1:def 14 :: thesis: for b1 being Element of the carrier of () holds (a + b) * b1 = (a * b1) + (b * b1)
let v be Vector of (); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider K = v as Linear_Combination of V by Def29;
A7: ( a * v = a * K & b * v = b * K ) by A4;
(a + b) * v = (a + b) * K by A4
.= (a * K) + (b * K) by Th32
.= (a * v) + (b * v) by A1, A7 ;
hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum
end;
thus LC_Z_Module V is scalar-associative :: thesis:
proof
let a, b be Element of R; :: according to VECTSP_1:def 15 :: thesis: for b1 being Element of the carrier of () holds (a * b) * b1 = a * (b * b1)
let v be Vector of (); :: thesis: (a * b) * v = a * (b * v)
reconsider K = v as Linear_Combination of V by Def29;
A8: b * v = b * K by A4;
(a * b) * v = (a * b) * K by A4
.= a * (b * K) by Th34
.= a * (b * v) by A4, A8 ;
hence (a * b) * v = a * (b * v) ; :: thesis: verum
end;
let v be Vector of (); :: according to VECTSP_1:def 16 :: thesis: (1. R) * v = v
reconsider K = v as Linear_Combination of V by Def29;
thus (1. R) * v = (1. R) * K by A4
.= v ; :: thesis: verum