let L be non empty right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of L
for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q
let p, q be Polynomial of L; :: thesis: for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q
let n be Element of NAT ; :: thesis: ( n is_at_least_length_of p & n is_at_least_length_of q implies n is_at_least_length_of p + q )
assume A1: ( n is_at_least_length_of p & n is_at_least_length_of q ) ; :: thesis: n is_at_least_length_of p + q
let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not n <= i or (p + q) . i = 0. L )
assume i >= n ; :: thesis: (p + q) . i = 0. L
then A2: ( p . i = 0. L & q . i = 0. L ) by A1;
thus (p + q) . i = (0. L) + (0. L) by A2, NORMSP_1:def 2
.= 0. L by RLVECT_1:def 4 ; :: thesis: verum