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 A1: ( x = p & y = q ) ; :: thesis: x - y = p - q
then A2: - y = - q by Th15;
thus x - y = x + (- y) by RLVECT_1:def 12
.= p - q by A1, A2, POLYNOM3:def 12 ; :: thesis: verum