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 3
.= b + (0. (Polynom-Ring L)) by RLVECT_1:5
.= b by RLVECT_1:4 ; :: 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: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