now

thus for a, b being Element of (Polynom-Ring L) ex x being Element of (Polynom-Ring L) st a + x = b by RLVECT_1:20; :: thesis: ( ( for a, b being Element of (Polynom-Ring L) ex x being Element of (Polynom-Ring L) st x + a = b ) & ( for a, x, y being Element of (Polynom-Ring L) st a + x = a + y holds
x = y ) & ( for a, x, y being Element of (Polynom-Ring L) st x + a = y + a holds
x = y ) )
thus for a, b being Element of (Polynom-Ring L) ex x being Element of (Polynom-Ring L) st x + a = b :: thesis: ( ( for a, x, y being Element of (Polynom-Ring L) st a + x = a + y holds
x = y ) & ( for a, x, y being Element of (Polynom-Ring L) st x + a = y + a holds
x = y ) )

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;

thus for a, x, y being Element of (Polynom-Ring L) st a + x = a + y holds
x = y by RLVECT_1:21; :: thesis: for a, x, y being Element of (Polynom-Ring L) st x + a = y + a holds
x = y
thus for a, x, y being Element of (Polynom-Ring L) st x + a = y + a holds
x = y by RLVECT_1:21; :: thesis: verum

end;

hence Polynom-Ring L is Loop-like by ALGSTR_1:7; :: thesis: verum