A1:
for a, b being Element of (Polynom-Ring L) ex x being Element of (Polynom-Ring L) st x + a = b

x = y by RLVECT_1:8;

( ( for a, b being Element of (Polynom-Ring L) ex x being Element of (Polynom-Ring L) st a + x = b ) & ( for a, x, y being Element of (Polynom-Ring L) st a + x = a + y holds

x = y ) ) by RLVECT_1:7, RLVECT_1:8;

hence Polynom-Ring L is Loop-like by A1, A2, ALGSTR_1:6; :: thesis: verum

proof

A2:
for a, x, y being Element of (Polynom-Ring L) st x + a = y + a holds
let a, b be Element of (Polynom-Ring L); :: thesis: ex x being Element of (Polynom-Ring L) st x + a = b

reconsider x = b - a as Element of (Polynom-Ring L) ;

take x ; :: thesis: x + a = b

thus x + a = b + ((- a) + a) by RLVECT_1:def 3

.= b + (0. (Polynom-Ring L)) by RLVECT_1:5

.= b by RLVECT_1:4 ; :: thesis: verum

end;reconsider x = b - a as Element of (Polynom-Ring L) ;

take x ; :: thesis: x + a = b

thus x + a = b + ((- a) + a) by RLVECT_1:def 3

.= b + (0. (Polynom-Ring L)) by RLVECT_1:5

.= b by RLVECT_1:4 ; :: thesis: verum

x = y by RLVECT_1:8;

( ( for a, b being Element of (Polynom-Ring L) ex x being Element of (Polynom-Ring L) st a + x = b ) & ( for a, x, y being Element of (Polynom-Ring L) st a + x = a + y holds

x = y ) ) by RLVECT_1:7, RLVECT_1:8;

hence Polynom-Ring L is Loop-like by A1, A2, ALGSTR_1:6; :: thesis: verum