let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of L st len p <> len q holds
len (p + q) = max ((len p),(len q))
let p, q be Polynomial of L; :: thesis: ( len p <> len q implies len (p + q) = max ((len p),(len q)) )
assume A1: len p <> len q ; :: thesis: len (p + q) = max ((len p),(len q))

per cases ( len p < len q or len p > len q ) by A1, XXREAL_0:1;

suppose A2: len p < len q ; :: thesis: len (p + q) = max ((len p),(len q))

then len q >= (len p) + 1 by NAT_1:13;
then (len q) - 1 >= len p by XREAL_1:19;
then A3: (len q) -' 1 >= len p by XREAL_0:def 2;
len q >= 0 + 1 by A2, NAT_1:13;
then A4: len q = ((len q) -' 1) + 1 by XREAL_1:235;
A5: (p + q) . ((len q) -' 1) = (p . ((len q) -' 1)) + (q . ((len q) -' 1)) by NORMSP_1:def 2
.= (0. L) + (q . ((len q) -' 1)) by A3, ALGSEQ_1:8
.= q . ((len q) -' 1) by RLVECT_1:4 ;
A6: len (p + q) >= len q

proof

assume len (p + q) < len q ; :: thesis: contradiction
then (len (p + q)) + 1 <= len q by NAT_1:13;
then len (p + q) <= (len q) - 1 by XREAL_1:19;
then len (p + q) <= (len q) -' 1 by XREAL_0:def 2;
then (p + q) . ((len q) -' 1) = 0. L by ALGSEQ_1:8;
hence contradiction by A5, A4, ALGSEQ_1:10; :: thesis: verum

end;

( max ((len p),(len q)) = len q & len (p + q) <= len q ) by A2, Th6, XXREAL_0:def 10;
hence len (p + q) = max ((len p),(len q)) by A6, XXREAL_0:1; :: thesis: verum

end;

suppose A7: len p > len q ; :: thesis: len (p + q) = max ((len p),(len q))

then len p >= (len q) + 1 by NAT_1:13;
then (len p) - 1 >= len q by XREAL_1:19;
then A8: (len p) -' 1 >= len q by XREAL_0:def 2;
len p >= 0 + 1 by A7, NAT_1:13;
then A9: len p = ((len p) -' 1) + 1 by XREAL_1:235;
A10: (p + q) . ((len p) -' 1) = (p . ((len p) -' 1)) + (q . ((len p) -' 1)) by NORMSP_1:def 2
.= (p . ((len p) -' 1)) + (0. L) by A8, ALGSEQ_1:8
.= p . ((len p) -' 1) by RLVECT_1:4 ;
A11: len (p + q) >= len p

proof

assume len (p + q) < len p ; :: thesis: contradiction
then (len (p + q)) + 1 <= len p by NAT_1:13;
then len (p + q) <= (len p) - 1 by XREAL_1:19;
then len (p + q) <= (len p) -' 1 by XREAL_0:def 2;
then (p + q) . ((len p) -' 1) = 0. L by ALGSEQ_1:8;
hence contradiction by A10, A9, ALGSEQ_1:10; :: thesis: verum

end;

( max ((len p),(len q)) = len p & len (p + q) <= len p ) by A7, Th6, XXREAL_0:def 10;
hence len (p + q) = max ((len p),(len q)) by A11, XXREAL_0:1; :: thesis: verum

end;

end;