let L be non empty right_complementable add-associative right_zeroed distributive left_unital associative doubleLoopStr ; :: thesis: for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds
len (p *' q) = ((len p) + (len q)) - 1
let p, q be Polynomial of L; :: thesis: ( (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L implies len (p *' q) = ((len p) + (len q)) - 1 )
A1: ((len p) + (len q)) -' 1 is_at_least_length_of p *' q

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not ((len p) + (len q)) -' 1 <= i or (p *' q) . i = 0. L )
i in NAT by ORDINAL1:def 12;
then consider r being FinSequence of the carrier of L such that
A2: len r = i + 1 and
A3: (p *' q) . i = Sum r and
A4: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def 9;
assume i >= ((len p) + (len q)) -' 1 ; :: thesis: (p *' q) . i = 0. L
then i >= ((len p) + (len q)) - 1 by XREAL_0:def 2;
then i + 1 >= (len p) + (len q) by XREAL_1:20;
then len p <= (i + 1) - (len q) by XREAL_1:19;
then A5: - (len p) >= - ((i + 1) - (len q)) by XREAL_1:24;

now :: thesis: for k being Element of NAT st k in dom r holds
r . k = 0. L

let k be Element of NAT ; :: thesis: ( k in dom r implies r . b₁ = 0. L )
assume A6: k in dom r ; :: thesis: r . b₁ = 0. L
then A7: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A4;
k in Seg (len r) by A6, FINSEQ_1:def 3;
then k <= i + 1 by A2, FINSEQ_1:1;
then A8: (i + 1) - k >= 0 by XREAL_1:48;

per cases ( k -' 1 < len p or k -' 1 >= len p ) ;

suppose k -' 1 < len p ; :: thesis: r . b₁ = 0. L

then k - 1 < len p by XREAL_0:def 2;
then - (k - 1) > - (len p) by XREAL_1:24;
then 1 - k > (len q) - (i + 1) by A5, XXREAL_0:2;
then (i + 1) + (1 - k) > len q by XREAL_1:19;
then ((i + 1) - k) + 1 > len q ;
then ((i + 1) -' k) + 1 > len q by A8, XREAL_0:def 2;
then (i + 1) -' k >= len q by NAT_1:13;
then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8;
hence r . k = 0. L by A7; :: thesis: verum

end;

suppose k -' 1 >= len p ; :: thesis: r . b₁ = 0. L

then p . (k -' 1) = 0. L by ALGSEQ_1:8;
hence r . k = 0. L by A7; :: thesis: verum

end;

end;

end;

hence (p *' q) . i = 0. L by A3, POLYNOM3:1; :: thesis: verum

end;

assume A9: (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L ; :: thesis: len (p *' q) = ((len p) + (len q)) - 1

A10: now :: thesis: not len p <= 0

assume len p <= 0 ; :: thesis: contradiction
then len p = 0 ;
then p = 0_. L by Th5;
then p . ((len p) -' 1) = 0. L by FUNCOP_1:7;
hence contradiction by A9; :: thesis: verum

end;

A11: now :: thesis: not len q <= 0

assume len q <= 0 ; :: thesis: contradiction
then len q = 0 ;
then q = 0_. L by Th5;
then q . ((len q) -' 1) = 0. L by FUNCOP_1:7;
hence contradiction by A9; :: thesis: verum

end;

then (len p) + (len q) >= 0 + 1 by NAT_1:13;
then A12: ((len p) + (len q)) - 1 >= 1 - 1 by XREAL_1:9;

now :: thesis: for n being Nat st n is_at_least_length_of p *' q holds
not ((len p) + (len q)) -' 1 > n

let n be Nat; :: thesis: ( n is_at_least_length_of p *' q implies not ((len p) + (len q)) -' 1 > n )
assume that
A13: n is_at_least_length_of p *' q and
A14: ((len p) + (len q)) -' 1 > n ; :: thesis: contradiction
((len p) + (len q)) -' 1 >= n + 1 by A14, NAT_1:13;
then A15: (((len p) + (len q)) -' 1) - 1 >= n by XREAL_1:19;
A16: (((len p) + (len q)) -' 1) - 1 = (((len p) + (len q)) - 1) - 1 by A12, XREAL_0:def 2;
A17: len q >= 0 + 1 by A11, NAT_1:13;
then A18: (len q) - 1 >= 0 by XREAL_1:19;
(len p) + (len q) > 0 + 1 by A10, A17, XREAL_1:8;
then (len p) + (len q) >= 1 + 1 by NAT_1:13;
then A19: ((len p) + (len q)) - 2 >= 2 - 2 by XREAL_1:9;
then A20: ((len p) + (len q)) -' 2 = ((len p) + (len q)) - (1 + 1) by XREAL_0:def 2;
consider r being FinSequence of the carrier of L such that
A21: len r = (((len p) + (len q)) -' 2) + 1 and
A22: (p *' q) . (((len p) + (len q)) -' 2) = Sum r and
A23: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . (((((len p) + (len q)) -' 2) + 1) -' k)) by POLYNOM3:def 9;
A24: len r = ((((len p) + (len q)) - 1) + (- 1)) + 1 by A21, A19, XREAL_0:def 2
.= (len p) + ((len q) - 1) ;
then A25: ((((len p) + (len q)) -' 2) + 1) -' (len p) = ((((len p) + (len q)) -' 2) + 1) - (len p) by A21, A18, XREAL_0:def 2
.= (len q) -' 1 by A21, A18, A24, XREAL_0:def 2 ;
(len r) - (len p) = (len q) - 1 by A24;
then A26: (len p) + 0 <= len r by A18, XREAL_1:19;

now :: thesis: for i being Element of NAT st i in dom (r /^ (len p)) holds
(r /^ (len p)) . i = 0. L

let i be Element of NAT ; :: thesis: ( i in dom (r /^ (len p)) implies (r /^ (len p)) . i = 0. L )
assume A27: i in dom (r /^ (len p)) ; :: thesis: (r /^ (len p)) . i = 0. L
then A28: i in Seg (len (r /^ (len p))) by FINSEQ_1:def 3;
then A29: 1 <= i by FINSEQ_1:1;
i + (len p) >= i by NAT_1:11;
then i + (len p) >= 0 + 1 by A29, XXREAL_0:2;
then (i + (len p)) - 1 >= 0 by XREAL_1:19;
then A30: (i + (len p)) -' 1 = (len p) + (i - 1) by XREAL_0:def 2;
0 + 1 <= i by A28, FINSEQ_1:1;
then i - 1 >= 0 by XREAL_1:19;
then A31: (i + (len p)) -' 1 >= (len p) + 0 by A30, XREAL_1:6;
i <= len (r /^ (len p)) by A28, FINSEQ_1:1;
then i <= (len r) - (len p) by A26, RFINSEQ:def 1;
then A32: i + (len p) <= len r by XREAL_1:19;
i + (len p) >= i by NAT_1:11;
then i + (len p) >= 1 by A29, XXREAL_0:2;
then i + (len p) in Seg (len r) by A32, FINSEQ_1:1;
then A33: i + (len p) in dom r by FINSEQ_1:def 3;
thus (r /^ (len p)) . i = r . (i + (len p)) by A26, A27, RFINSEQ:def 1
.= (p . ((i + (len p)) -' 1)) * (q . (((((len p) + (len q)) -' 2) + 1) -' (i + (len p)))) by A23, A33
.= (0. L) * (q . (((((len p) + (len q)) -' 2) + 1) -' (i + (len p)))) by A31, ALGSEQ_1:8
.= 0. L ; :: thesis: verum

end;

then A34: Sum (r /^ (len p)) = 0. L by POLYNOM3:1;
A35: len p >= 0 + 1 by A10, NAT_1:13;
then len p in Seg (len r) by A26, FINSEQ_1:1;
then A36: len p in dom r by FINSEQ_1:def 3;

now :: thesis: for i being Element of NAT st i in dom (r | ((len p) -' 1)) holds
(r | ((len p) -' 1)) . i = 0. L

A37: (len p) - 1 >= 1 - 1 by A35, XREAL_1:9;
A38: (((len p) + (len q)) -' 2) + 1 = ((len p) - 1) + (len q) by A21, A24
.= ((len p) -' 1) + (len q) by A37, XREAL_0:def 2 ;
A39: dom (r | ((len p) -' 1)) c= dom r by FINSEQ_5:18;
let i be Element of NAT ; :: thesis: ( i in dom (r | ((len p) -' 1)) implies (r | ((len p) -' 1)) . i = 0. L )
assume A40: i in dom (r | ((len p) -' 1)) ; :: thesis: (r | ((len p) -' 1)) . i = 0. L
len p < (len r) + 1 by A26, NAT_1:13;
then (len p) - 1 < ((len r) + 1) - 1 by XREAL_1:9;
then (len p) -' 1 < len r by A37, XREAL_0:def 2;
then len (r | ((len p) -' 1)) = (len p) -' 1 by FINSEQ_1:59;
then i in Seg ((len p) -' 1) by A40, FINSEQ_1:def 3;
then i <= (len p) -' 1 by FINSEQ_1:1;
then i + (len q) <= ((len p) -' 1) + (len q) by XREAL_1:6;
then len q <= ((((len p) + (len q)) -' 2) + 1) - i by A38, XREAL_1:19;
then A41: len q <= ((((len p) + (len q)) -' 2) + 1) -' i by XREAL_0:def 2;
thus (r | ((len p) -' 1)) . i = (r | ((len p) -' 1)) /. i by A40, PARTFUN1:def 6
.= r /. i by A40, FINSEQ_4:70
.= r . i by A40, A39, PARTFUN1:def 6
.= (p . (i -' 1)) * (q . (((((len p) + (len q)) -' 2) + 1) -' i)) by A23, A40, A39
.= (p . (i -' 1)) * (0. L) by A41, ALGSEQ_1:8
.= 0. L ; :: thesis: verum

end;

then A42: Sum (r | ((len p) -' 1)) = 0. L by POLYNOM3:1;
r = ((r | ((len p) -' 1)) ^ <*(r . (len p))*>) ^ (r /^ (len p)) by A26, A35, FINSEQ_5:84;
then r = ((r | ((len p) -' 1)) ^ <*(r /. (len p))*>) ^ (r /^ (len p)) by A26, A35, FINSEQ_4:15;
then Sum r = (Sum ((r | ((len p) -' 1)) ^ <*(r /. (len p))*>)) + (Sum (r /^ (len p))) by RLVECT_1:41
.= ((Sum (r | ((len p) -' 1))) + (Sum <*(r /. (len p))*>)) + (Sum (r /^ (len p))) by RLVECT_1:41 ;
then Sum r = (Sum <*(r /. (len p))*>) + (0. L) by A42, A34, RLVECT_1:4
.= Sum <*(r /. (len p))*> by RLVECT_1:4
.= r /. (len p) by RLVECT_1:44
.= r . (len p) by A36, PARTFUN1:def 6
.= (p . ((len p) -' 1)) * (q . ((len q) -' 1)) by A23, A36, A25 ;
hence contradiction by A9, A13, A22, A16, A20, A15; :: thesis: verum

end;

then len (p *' q) = ((len p) + (len q)) -' 1 by A1, ALGSEQ_1:def 3;
hence len (p *' q) = ((len p) + (len q)) - 1 by A12, XREAL_0:def 2; :: thesis: verum