set P = Polynom-Ring p;
set C = { q where q is Polynomial of F : deg q < deg p } ;
H0: { q where q is Polynomial of F : deg q < deg p } = the carrier of (Polynom-Ring p) by defprfp;
H1: 0. (Polynom-Ring p) = 0_. F by defprfp;

now :: thesis: for x, y being Element of (Polynom-Ring p) holds x + y = y + x

let x, y be Element of (Polynom-Ring p); :: thesis: x + y = y + x
x in the carrier of (Polynom-Ring p) ;
then x in { q where q is Polynomial of F : deg q < deg p } by defprfp;
then consider q being Polynomial of F such that
A1: ( x = q & deg q < deg p ) ;
y in the carrier of (Polynom-Ring p) ;
then y in { q where q is Polynomial of F : deg q < deg p } by defprfp;
then consider r being Polynomial of F such that
A2: ( y = r & deg r < deg p ) ;
reconsider q = q, r = r as Element of (Polynom-Ring F) by POLYNOM3:def 10;
A3: ( [x,y] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] & [y,x] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] ) by H0, ZFMISC_1:def 2;
thus x + y = ( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (x,y) by H0, defprfp
.= q + r by A1, A2, A3, FUNCT_1:49
.= the addF of (Polynom-Ring F) . (y,x) by A1, A2, ALGSTR_0:def 1
.= ( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (y,x) by A3, FUNCT_1:49
.= y + x by H0, defprfp ; :: thesis: verum

end;

hence Polynom-Ring p is Abelian by RLVECT_1:def 2; :: thesis: ( Polynom-Ring p is add-associative & Polynom-Ring p is right_zeroed & Polynom-Ring p is right_complementable )

now :: thesis: for x, y, z being Element of (Polynom-Ring p) holds x + (y + z) = (x + y) + z

let x, y, z be Element of (Polynom-Ring p); :: thesis: x + (y + z) = (x + y) + z
x in the carrier of (Polynom-Ring p) ;
then x in { q where q is Polynomial of F : deg q < deg p } by defprfp;
then consider q being Polynomial of F such that
A1: ( x = q & deg q < deg p ) ;
y in the carrier of (Polynom-Ring p) ;
then y in { q where q is Polynomial of F : deg q < deg p } by defprfp;
then consider r being Polynomial of F such that
A2: ( y = r & deg r < deg p ) ;
z in the carrier of (Polynom-Ring p) ;
then z in { q where q is Polynomial of F : deg q < deg p } by defprfp;
then consider u being Polynomial of F such that
A3: ( z = u & deg u < deg p ) ;
A3a: ( [x,y] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] & [y,z] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] ) by H0, ZFMISC_1:def 2;
A3b: ( [(x + y),z] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] & [x,(y + z)] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] ) by H0, ZFMISC_1:def 2;
reconsider q = q, r = r, u = u as Element of (Polynom-Ring F) by POLYNOM3:def 10;
A4: x + y = ( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (x,y) by H0, defprfp
.= q + r by A1, A2, A3a, FUNCT_1:49 ;
A5: y + z = ( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (y,z) by H0, defprfp
.= r + u by A3, A2, A3a, FUNCT_1:49 ;
A6: (x + y) + z = ( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . ((x + y),z) by H0, defprfp
.= (q + r) + u by A3, A4, A3b, FUNCT_1:49
.= q + (r + u) by RLVECT_1:def 3 ;
thus x + (y + z) = ( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (x,(y + z)) by H0, defprfp
.= (x + y) + z by A6, A5, A1, A3b, FUNCT_1:49 ; :: thesis: verum

end;

hence Polynom-Ring p is add-associative by RLVECT_1:def 3; :: thesis: ( Polynom-Ring p is right_zeroed & Polynom-Ring p is right_complementable )

now :: thesis: for x being Element of (Polynom-Ring p) holds x + (0. (Polynom-Ring p)) = x

let x be Element of (Polynom-Ring p); :: thesis: x + (0. (Polynom-Ring p)) = x
x in the carrier of (Polynom-Ring p) ;
then x in { q where q is Polynomial of F : deg q < deg p } by defprfp;
then consider q being Polynomial of F such that
A1: ( x = q & deg q < deg p ) ;
reconsider q1 = q as Element of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider r = 0_. F as Element of (Polynom-Ring F) by POLYNOM3:def 10;
A3: [x,(0. (Polynom-Ring p))] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] by H0, ZFMISC_1:def 2;
thus x + (0. (Polynom-Ring p)) = ( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (x,(0. (Polynom-Ring p))) by H0, defprfp
.= the addF of (Polynom-Ring F) . (x,(0. (Polynom-Ring p))) by A3, FUNCT_1:49
.= q1 + r by defprfp, A1
.= q + (0_. F) by POLYNOM3:def 10
.= x by A1, POLYNOM3:28 ; :: thesis: verum

end;

hence Polynom-Ring p is right_zeroed by RLVECT_1:def 4; :: thesis: Polynom-Ring p is right_complementable

now :: thesis: for x being Element of (Polynom-Ring p) holds x is right_complementable

let x be Element of (Polynom-Ring p); :: thesis: x is right_complementable
x in the carrier of (Polynom-Ring p) ;
then x in { q where q is Polynomial of F : deg q < deg p } by defprfp;
then consider q being Polynomial of F such that
A1: ( x = q & deg q < deg p ) ;
reconsider q1 = q as Element of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider r = - q as Element of (Polynom-Ring F) by POLYNOM3:def 10;
deg (- q) = deg q by POLYNOM4:8;
then - q in { q where q is Polynomial of F : deg q < deg p } by A1;
then reconsider y = - q as Element of (Polynom-Ring p) by defprfp;
A3: [x,y] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] by H0, ZFMISC_1:def 2;
x + y = ( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (x,y) by H0, defprfp
.= q1 + r by A1, A3, FUNCT_1:49
.= q - q by POLYNOM3:def 10
.= 0_. F by POLYNOM3:29 ;
hence x is right_complementable by H1; :: thesis: verum

end;

hence Polynom-Ring p is right_complementable ; :: thesis: verum