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 A3: max (len p),(len q) = len q by XXREAL_0:def 10;
A4: len q >= 0 + 1 by A2, NAT_1:13;
len q >= (len p) + 1 by A2, NAT_1:13;
then (len q) - 1 >= len p by XREAL_1:21;
then A5: (len q) -' 1 >= len p by XREAL_0:def 2;
A6: (p + q) . ((len q) -' 1) = (p . ((len q) -' 1)) + (q . ((len q) -' 1)) by NORMSP_1:def 5
.= (0. L) + (q . ((len q) -' 1)) by A5, ALGSEQ_1:22
.= q . ((len q) -' 1) by RLVECT_1:10 ;
A7: len q = ((len q) -' 1) + 1 by A4, XREAL_1:237;
A8: len (p + q) <= len q by A2, Th9;
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:21;
then len (p + q) <= (len q) -' 1 by XREAL_0:def 2;
then (p + q) . ((len q) -' 1) = 0. L by ALGSEQ_1:22;
hence contradiction by A6, A7, ALGSEQ_1:25; :: thesis: verum

end;

hence len (p + q) = max (len p),(len q) by A3, A8, XXREAL_0:1; :: thesis: verum

end;

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

then A10: max (len p),(len q) = len p by XXREAL_0:def 10;
A11: len p >= 0 + 1 by A9, NAT_1:13;
len p >= (len q) + 1 by A9, NAT_1:13;
then (len p) - 1 >= len q by XREAL_1:21;
then A12: (len p) -' 1 >= len q by XREAL_0:def 2;
A13: (p + q) . ((len p) -' 1) = (p . ((len p) -' 1)) + (q . ((len p) -' 1)) by NORMSP_1:def 5
.= (p . ((len p) -' 1)) + (0. L) by A12, ALGSEQ_1:22
.= p . ((len p) -' 1) by RLVECT_1:10 ;
A14: len p = ((len p) -' 1) + 1 by A11, XREAL_1:237;
A15: len (p + q) <= len p by A9, Th9;
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:21;
then len (p + q) <= (len p) -' 1 by XREAL_0:def 2;
then (p + q) . ((len p) -' 1) = 0. L by ALGSEQ_1:22;
hence contradiction by A13, A14, ALGSEQ_1:25; :: thesis: verum

end;

hence len (p + q) = max (len p),(len q) by A10, A15, XXREAL_0:1; :: thesis: verum

end;

end;