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

proof

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 6
.= b + (0. (Polynom-Ring L)) by RLVECT_1:16
.= b by RLVECT_1:10 ; :: thesis: verum

end;

A2: for a, x, y being Element of (Polynom-Ring L) st x + a = y + a holds
x = y by RLVECT_1:21;
( ( 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:20, RLVECT_1:21;
hence Polynom-Ring L is Loop-like by A1, A2, ALGSTR_1:7; :: thesis: verum