let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for p, q being Polynomial of L st p <> 0_. L & q <> 0_. L holds
(p *' q) . ((((len p) + (len q)) - 1) -' 1) = (p . ((len p) -' 1)) * (q . ((len q) -' 1))
let p, q be Polynomial of L; :: thesis: ( p <> 0_. L & q <> 0_. L implies (p *' q) . ((((len p) + (len q)) - 1) -' 1) = (p . ((len p) -' 1)) * (q . ((len q) -' 1)) )
assume ( p <> 0_. L & q <> 0_. L ) ; :: thesis: (p *' q) . ((((len p) + (len q)) - 1) -' 1) = (p . ((len p) -' 1)) * (q . ((len q) -' 1))
then B: ( len p >= 1 & len q >= 1 ) by NAT_1:14, POLYNOM4:5;
then (len p) + (len q) >= 1 + 1 by XREAL_1:7;
then A: ((len p) + (len q)) - 1 >= (1 + 1) - 1 by XREAL_1:9;
reconsider j = ((len p) + (len q)) - 1 as Element of NAT by B, INT_1:3;
set i = j -' 1;
consider r being FinSequence of the carrier of L such that
M: ( len r = (j -' 1) + 1 & (p *' q) . (j -' 1) = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . (((j -' 1) + 1) -' k)) ) ) by POLYNOM3:def 9;
A7: j - 1 = j -' 1 by A, XREAL_0:def 2;
reconsider x = (len q) - 1 as Element of NAT by B, INT_1:3;
A3: j = (len p) + x ;
then j >= len p by NAT_1:11;
then A1: len p in dom r by A7, M, B, FINSEQ_3:25;
A2: ((j -' 1) + 1) -' (len p) = (((((len p) + (len q)) - 1) - 1) + 1) - (len p) by A3, A7, XREAL_0:def 2
.= (((len p) - (len p)) + (len q)) - 1
.= (len q) -' 1 by B, XREAL_0:def 2 ;

now :: thesis: for k being Element of NAT st k in dom r & k <> len p holds
r /. k = 0. L

let k be Element of NAT ; :: thesis: ( k in dom r & k <> len p implies r /. b₁ = 0. L )
assume E: ( k in dom r & k <> len p ) ; :: thesis: r /. b₁ = 0. L

per cases ( k > len p or k < len p ) by E, XXREAL_0:1;

suppose E1: k > len p ; :: thesis: r /. b₁ = 0. L

then reconsider k1 = k - 1 as Element of NAT by INT_1:3;
E2: k1 + 1 > len p by E1;
k -' 1 = k - 1 by E1, XREAL_0:def 2;
then p . (k -' 1) = 0. L by E2, ALGSEQ_1:8, NAT_1:13;
then r . k = (0. L) * (q . (((j -' 1) + 1) -' k)) by E, M;
hence r /. k = 0. L by E, PARTFUN1:def 6; :: thesis: verum

end;

suppose k < len p ; :: thesis: r /. b₁ = 0. L

then k + 1 <= len p by INT_1:7;
then (k + 1) - k <= (len p) - k by XREAL_1:9;
then ((len p) - k) + (len q) >= 1 + (len q) by XREAL_1:6;
then E2: (((len p) - k) + (len q)) - 1 >= ((len q) + 1) - 1 by XREAL_1:9;
((j -' 1) + 1) - k = (((((len p) + (len q)) - 1) - 1) + 1) - k by A, XREAL_0:def 2;
then ((j -' 1) + 1) -' k = (((len p) + (len q)) - 1) - k by E2, XREAL_0:def 2;
then q . (((j -' 1) + 1) -' k) = 0. L by E2, ALGSEQ_1:8;
then r . k = (p . (k -' 1)) * (0. L) by E, M;
hence r /. k = 0. L by E, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

then Sum r = r /. (len p) by A1, POLYNOM2:3
.= r . (len p) by A1, PARTFUN1:def 6
.= (p . ((len p) -' 1)) * (q . (((j -' 1) + 1) -' (len p))) by A1, M ;
hence (p *' q) . ((((len p) + (len q)) - 1) -' 1) = (p . ((len p) -' 1)) * (q . ((len q) -' 1)) by M, A2; :: thesis: verum