let R be domRing; :: thesis: for p, q being non zero Polynomial of R holds min* { i where i is Nat : (p *' q) . i <> 0. R } = (min* { i where i is Nat : p . i <> 0. R } ) + (min* { i where i is Nat : q . i <> 0. R } )
let p, q be non zero Polynomial of R; :: thesis: min* { i where i is Nat : (p *' q) . i <> 0. R } = (min* { i where i is Nat : p . i <> 0. R } ) + (min* { i where i is Nat : q . i <> 0. R } )
reconsider cp = { i where i is Nat : p . i <> 0. R } , cq = { i where i is Nat : q . i <> 0. R } , cpq = { i where i is Nat : (p *' q) . i <> 0. R } as non empty Subset of NAT by lemlp1;
set m = (min* cp) + (min* cq);
consider r being FinSequence of the carrier of R such that
M: ( len r = ((min* cp) + (min* cq)) + 1 & (p *' q) . ((min* cp) + (min* cq)) = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((((min* cp) + (min* cq)) + 1) -' k)) ) ) by POLYNOM3:def 9;
B1: 1 <= (min* cp) + 1 by NAT_1:11;
(min* cp) + 1 <= ((min* cp) + 1) + (min* cq) by NAT_1:11;
then (min* cp) + 1 in Seg (((min* cp) + (min* cq)) + 1) by B1, FINSEQ_1:1;
then A1: (min* cp) + 1 in dom r by M, FINSEQ_1:def 3;
A2: ((min* cp) + 1) - 1 >= 0 ;
A4: (((min* cp) + (min* cq)) + 1) -' ((min* cp) + 1) = (((min* cp) + (min* cq)) + 1) - ((min* cp) + 1) by XREAL_0:def 2;

now :: thesis: for k being Element of NAT st k in dom r & k <> (min* cp) + 1 holds
r /. k = 0. R

let k be Element of NAT ; :: thesis: ( k in dom r & k <> (min* cp) + 1 implies r /. b₁ = 0. R )
assume E: ( k in dom r & k <> (min* cp) + 1 ) ; :: thesis: r /. b₁ = 0. R
then EE: ( 1 <= k & k <= ((min* cp) + (min* cq)) + 1 ) by M, FINSEQ_3:25;

per cases ( k < (min* cp) + 1 or k > (min* cp) + 1 ) by E, XXREAL_0:1;

suppose E1: k < (min* cp) + 1 ; :: thesis: r /. b₁ = 0. R

reconsider k1 = k - 1 as Element of NAT by EE, INT_1:3;
E4: k -' 1 = k - 1 by EE, XREAL_0:def 2;
then E3: k -' 1 < ((min* cp) + 1) - 1 by E1, XREAL_1:9;

now :: thesis: not p . k1 <> 0. R

assume p . k1 <> 0. R ; :: thesis: contradiction
then k1 in cp ;
hence contradiction by E3, E4, NAT_1:def 1; :: thesis: verum

end;

then r . k = (0. R) * (q . ((((min* cp) + (min* cq)) + 1) -' k)) by E4, E, M;
hence r /. k = 0. R by E, PARTFUN1:def 6; :: thesis: verum

end;

suppose k > (min* cp) + 1 ; :: thesis: r /. b₁ = 0. R

then E1: (((min* cp) + (min* cq)) + 1) - k < (((min* cp) + (min* cq)) + 1) - ((min* cp) + 1) by XREAL_1:10;
(((min* cp) + (min* cq)) + 1) - k in NAT by EE, INT_1:5;
then E3: (((min* cp) + (min* cq)) + 1) -' k < min* cq by E1, XREAL_0:def 2;

now :: thesis: not q . ((((min* cp) + (min* cq)) + 1) -' k) <> 0. R

assume q . ((((min* cp) + (min* cq)) + 1) -' k) <> 0. R ; :: thesis: contradiction
then (((min* cp) + (min* cq)) + 1) -' k in cq ;
hence contradiction by E3, NAT_1:def 1; :: thesis: verum

end;

then r . k = (p . (k -' 1)) * (0. R) by E, M;
hence r /. k = 0. R by E, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

then X: Sum r = r /. ((min* cp) + 1) by A1, POLYNOM2:3
.= r . ((min* cp) + 1) by A1, PARTFUN1:def 6
.= (p . (((min* cp) + 1) -' 1)) * (q . ((((min* cp) + (min* cq)) + 1) -' ((min* cp) + 1))) by A1, M
.= (p . (min* cp)) * (q . (min* cq)) by A4, A2, XREAL_0:def 2 ;
min* cp in cp by NAT_1:def 1;
then consider u being Nat such that
H1: ( u = min* cp & p . u <> 0. R ) ;
min* cq in cq by NAT_1:def 1;
then consider v being Nat such that
H2: ( v = min* cq & q . v <> 0. R ) ;
(p . u) * (q . v) <> 0. R by H1, H2, VECTSP_2:def 1;
then (min* cp) + (min* cq) in { i where i is Nat : (p *' q) . i <> 0. R } by H1, H2, X, M;
then C1: min* cpq <= (min* cp) + (min* cq) by NAT_1:def 1;
p *' q <> 0_. R ;
then min* cpq >= (min* cp) + (min* cq) by lemlowp3a;
hence min* { i where i is Nat : (p *' q) . i <> 0. R } = (min* { i where i is Nat : p . i <> 0. R } ) + (min* { i where i is Nat : q . i <> 0. R } ) by C1, XXREAL_0:1; :: thesis: verum