let R be Ring; :: thesis:
set a = 0. Trivial-addLoopStr ;
set G = VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #);
A1: for a, b being Element of
for x, y being Element of st x = a & b = y holds
a + b = x + y ;
A2: ( VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #) is Abelian & VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #) is add-associative & VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #) is right_zeroed & VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #) is right_complementable )

let a, b be Element of ; :: according to RLVECT_1:def 5 :: thesis:
reconsider x = a, y = b as Element of ;
thus a + b = y + x by A1
.= b + a ; :: thesis:

end;

let a, b, c be Element of ; :: thesis:
reconsider x = a, y = b, z = c as Element of ;
thus (a + b) + c = (x + y) + z
.= x + (y + z) by RLVECT_1:def 6
.= a + (b + c) ; :: thesis:

end;

let a be Element of ; :: thesis:
reconsider x = a as Element of ;
thus a + (0. VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #)) = x + (0. Trivial-addLoopStr )
.= a by RLVECT_1:10 ; :: thesis:

end;

let a be Element of ; :: according to ALGSTR_0:def 16 :: thesis:
reconsider x = a as Element of ;
consider b being Element of such that
A3: x + b = 0. Trivial-addLoopStr by ALGSTR_0:def 11;
reconsider b' = b as Element of ;
take b' ; :: according to ALGSTR_0:def 11 :: thesis:
thus a + b' = 0. VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #) by A3; :: thesis:

end;

let x, y be Scalar of ; :: thesis:
let v, w be Vector of ; :: thesis:
A4: ( (x * y) * v = 0. Trivial-addLoopStr & (1. R) * v = 0. Trivial-addLoopStr ) by GRCAT_1:8;
( x * (v + w) = 0. Trivial-addLoopStr & (x + y) * v = 0. Trivial-addLoopStr ) by GRCAT_1:8;
hence ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v ) by A4, GRCAT_1:8; :: thesis:

end;