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 that
A1: n >= len p and
A2: n >= len q ; :: thesis: n >= len (p + q)
( n is_at_least_length_of p & n is_at_least_length_of q ) by A1, A2, POLYNOM3:23;
then n is_at_least_length_of p + q by POLYNOM3:24;
hence n >= len (p + q) by POLYNOM3:23; :: thesis: verum