let L be non empty 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 ( n >= len p & n >= len q ) ; :: thesis: n >= len (p + q)
then ( n is_at_least_length_of p & n is_at_least_length_of q ) by POLYNOM3:23;
then n is_at_least_length_of p + q by POLYNOM3:24;
hence n >= len (p + q) by POLYNOM3:23; :: thesis: verum