set V = R ^* n;

now :: thesis: for x, y being Element of the carrier of (R ^* n) holds x + y = y + x

let x, y be Element of the carrier of (R ^* n); :: thesis: x + y = y + x
reconsider u = x, v = y as Element of n -tuples_on the carrier of R by DEF;
thus x + y = (vector_add (n,R)) . (u,v) by DEF
.= u + v by Defa
.= v + u by Lm1
.= (vector_add (n,R)) . (v,u) by Defa
.= y + x by DEF ; :: thesis: verum

end;

hence R ^* n is Abelian by RLVECT_1:def 2; :: thesis: ( R ^* n is add-associative & R ^* n is right_zeroed & R ^* n is right_complementable )

now :: thesis: for x, y, z being Element of the carrier of (R ^* n) holds (x + y) + z = x + (y + z)

let x, y, z be Element of the carrier of (R ^* n); :: thesis: (x + y) + z = x + (y + z)
reconsider u = x, v = y, w = z as Element of n -tuples_on the carrier of R by DEF;
H: y + z = (vector_add (n,R)) . (v,w) by DEF
.= v + w by Defa ;
x + y = (vector_add (n,R)) . (u,v) by DEF
.= u + v by Defa ;
hence (x + y) + z = (vector_add (n,R)) . ((u + v),w) by DEF
.= (u + v) + w by Defa
.= u + (v + w) by Lm2
.= (vector_add (n,R)) . (u,(v + w)) by Defa
.= x + (y + z) by H, DEF ;
:: thesis: verum

end;

hence R ^* n is add-associative by RLVECT_1:def 3; :: thesis: ( R ^* n is right_zeroed & R ^* n is right_complementable )

now :: thesis: for x being Element of the carrier of (R ^* n) holds x + (0. (R ^* n)) = x

let x be Element of the carrier of (R ^* n); :: thesis: x + (0. (R ^* n)) = x
reconsider u = x as Element of n -tuples_on the carrier of R by DEF;
H: 0. (R ^* n) = n |-> (0. R) by DEF;
thus x + (0. (R ^* n)) = (vector_add (n,R)) . (u,(0. (R ^* n))) by DEF
.= u + (n |-> (0. R)) by H, Defa
.= x by FVSUM_1:21 ; :: thesis: verum

end;

hence R ^* n is right_zeroed by RLVECT_1:def 4; :: thesis: R ^* n is right_complementable

now :: thesis: for x being Element of (R ^* n) holds x is right_complementable

let x be Element of (R ^* n); :: thesis: x is right_complementable
reconsider u = x as Element of n -tuples_on the carrier of R by DEF;
reconsider y = - u as Element of (R ^* n) by DEF;
x + y = (vector_add (n,R)) . (u,(- u)) by DEF
.= u + (- u) by Defa
.= n |-> (0. R) by FVSUM_1:26
.= 0. (R ^* n) by DEF ;
hence x is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;

hence R ^* n is right_complementable by ALGSTR_0:def 16; :: thesis: verum