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)
let n be Element of NAT ; :: thesis: ( n >= len p & n >= len q implies n >= len (p - q) )
assume A1: ( n >= len p & n >= len q ) ; :: thesis: n >= len (p - q)
len q = len (- q) by Th11;
hence n >= len (p - q) by A1, Th9; :: thesis: verum