set F = R;
set Fp = R |^ p;
A1: ( 1. (R |^ p) = 1. R & 0. (R |^ p) = 0. R ) 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 Lm12
.= y * x by Lm12 ; :: thesis: verum

end;

hence R |^ p is commutative by GROUP_1:def 12; :: thesis: ( R |^ p is associative & R |^ p is well-unital & R |^ p is distributive )

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 Lm12;
x * y = a * b by Lm12;
hence (x * y) * z = (a * b) * c by Lm12
.= a * (b * c) by GROUP_1:def 3
.= x * (y * z) by A3, Lm12 ;
:: thesis: verum

end;

hence R |^ p is associative by GROUP_1:def 3; :: thesis: ( R |^ p is well-unital & R |^ p is distributive )

now :: thesis: for x being Element of (R |^ p) holds
( x * (1. (R |^ p)) = x & (1. (R |^ p)) * x = x )

let x be Element of (R |^ p); :: thesis: ( x * (1. (R |^ p)) = x & (1. (R |^ p)) * x = x )
reconsider a = x as Element of R by Lm10;
thus x * (1. (R |^ p)) = a * (1. R) by A1, Lm12
.= x ; :: thesis: (1. (R |^ p)) * x = x
thus (1. (R |^ p)) * x = (1. R) * a by A1, Lm12
.= x ; :: thesis: verum

end;

hence R |^ p is well-unital by VECTSP_1:def 6; :: thesis: R |^ p is distributive

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

let x, y, z be Element of (R |^ p); :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider a = x, b = y, c = z as Element of R by Lm10;
A4: ( a * b = x * y & a * c = x * z ) by Lm12;
A6: ( b * a = y * x & c * a = z * x ) by Lm12;
A5: y + z = b + c by Lm11;
hence x * (y + z) = a * (b + c) by Lm12
.= (a * b) + (a * c) by VECTSP_1:def 7
.= (x * y) + (x * z) by A4, Lm11 ;
:: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (b + c) * a by A5, Lm12
.= (b * a) + (c * a) by VECTSP_1:def 7
.= (y * x) + (z * x) by A6, Lm11 ; :: thesis: verum

end;

hence R |^ p is distributive by VECTSP_1:def 7; :: thesis: verum