set F = R;
set Fp = R |^ p;
A1: 0. (R |^ p) = 0. R by deffp;
A2: the carrier of (R |^ p) = { (a |^ p) where a is Element of R : verum } by deffp;

now :: thesis: for x, y being Element of (R |^ p) holds x + y = y + x

let x, y be Element of (R |^ p); :: thesis: x + y = y + x
reconsider a = x, b = y as Element of R by Lm10;
thus x + y = a + b by Lm11
.= y + x by Lm11 ; :: thesis: verum

end;

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

now :: thesis: for x, y, z being Element of (R |^ p) holds (x + y) + z = x + (y + z)

let x, y, z be Element of (R |^ p); :: thesis: (x + y) + z = x + (y + z)
reconsider a = x, b = y, c = z as Element of R by Lm10;
A3: y + z = b + c by Lm11;
x + y = a + b by Lm11;
hence (x + y) + z = (a + b) + c by Lm11
.= a + (b + c) by RLVECT_1:def 3
.= x + (y + z) by A3, Lm11 ;
:: thesis: verum

end;

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

now :: thesis: for x being Element of (R |^ p) holds x + (0. (R |^ p)) = x

let x be Element of (R |^ p); :: thesis: x + (0. (R |^ p)) = x
reconsider a = x as Element of R by Lm10;
thus x + (0. (R |^ p)) = a + (0. R) by A1, Lm11
.= x ; :: thesis: verum

end;

hence R |^ p is right_zeroed by RLVECT_1:def 4; :: thesis: R |^ p is right_complementable

now :: thesis: for x being Element of (R |^ p) holds x is right_complementable

let x be Element of (R |^ p); :: thesis: x is right_complementable
reconsider a = x as Element of R by Lm10;
x in the carrier of (R |^ p) ;
then consider b being Element of R such that
H: x = b |^ p by A2;
- a = (- b) |^ p by H, fresh2;
then - a in { (a |^ p) where a is Element of R : verum } ;
then reconsider y = - a as Element of (R |^ p) by deffp;
x + y = a + (- a) by Lm11
.= 0. (R |^ p) by A1, RLVECT_1:5 ;
hence x is right_complementable by ALGSTR_0:def 11; :: thesis: verum

end;

hence R |^ p is right_complementable by ALGSTR_0:def 16; :: thesis: verum