let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of L
for n being Element of NAT st n >= len p & n >= len q holds
n >= len (p - q)
let p, q be Polynomial of L; :: thesis: for n being Element of NAT st n >= len p & n >= len q holds
n >= len (p - q)
len q = len (- q) by Th8;
hence for n being Element of NAT st n >= len p & n >= len q holds
n >= len (p - q) by Th6; :: thesis: verum