let L be Ring; :: thesis: for a, b being Element of (Polynom-Ring L)
for p, q being Polynomial of L st a = p & b = q holds
a - b = p - q
let a, b be Element of (Polynom-Ring L); :: thesis: for p, q being Polynomial of L st a = p & b = q holds
a - b = p - q
let p, q be Polynomial of L; :: thesis: ( a = p & b = q implies a - b = p - q )
assume A1: ( a = p & b = q ) ; :: thesis: a - b = p - q
then - b = - q by Lm6;
hence a - b = p + (- q) by A1, POLYNOM3:def 10
.= p - q by POLYNOM3:def 6 ;
:: thesis: verum