let L be non empty right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q)
let p, q be Polynomial of L; :: thesis: support (p + q) c= (support p) \/ (support q)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support (p + q) or x in (support p) \/ (support q) )
assume A1: x in support (p + q) ; :: thesis: x in (support p) \/ (support q)
then reconsider x1 = x as Element of NAT ;
A2: x1 < len (p + q) by A1, ALGSEQ_1:10;
( x1 < len p or x1 < len q )

proof

assume that
A3: not x1 < len p and
A4: not x1 < len q ; :: thesis: contradiction
( x1 is_at_least_length_of p & x1 is_at_least_length_of q ) by A3, A4, Th23;
then x1 is_at_least_length_of p + q by Th24;
hence contradiction by A2, Th23; :: thesis: verum

end;

then ( x in Segm (len p) or x in Segm (len q) ) by NAT_1:45;
hence x in (support p) \/ (support q) by XBOOLE_0:def 3; :: thesis: verum