let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for x, y being Element of (Polynom-Ring L)
for p, q being sequence of L st x = p & y = q holds
x - y = p - q
let x, y be Element of (Polynom-Ring L); :: thesis: for p, q being sequence of L st x = p & y = q holds
x - y = p - q
let p, q be sequence of L; :: thesis: ( x = p & y = q implies x - y = p - q )
assume that
A1: x = p and
A2: y = q ; :: thesis: x - y = p - q
A3: - y = - q by A2, Th15;
thus x - y = x + (- y) by RLVECT_1:def 11
.= p - q by A1, A3, POLYNOM3:def 10 ; :: thesis: verum