let R be non degenerated Ring; :: thesis: for p, q being non zero Polynomial of R st p *' q <> 0_. 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: ( p *' q <> 0_. R implies 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 } as non empty Subset of NAT by lemlp1;
assume p *' q <> 0_. 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 } )
then not p *' q is zero ;
then reconsider 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);
A: min* cpq in cpq by NAT_1:def 1;

now :: thesis: for z1 being Nat st z1 in cpq holds
z1 >= (min* cp) + (min* cq)

let z1 be Nat; :: thesis: ( z1 in cpq implies z1 >= (min* cp) + (min* cq) )
assume z1 in cpq ; :: thesis: z1 >= (min* cp) + (min* cq)
then consider w being Nat such that
H1: ( w = z1 & (p *' q) . w <> 0. R ) ;
reconsider z = z1 as Element of NAT by ORDINAL1:def 12;
consider r1 being FinSequence of the carrier of R such that
R: ( len r1 = z + 1 & (p *' q) . z = Sum r1 & ( for k being Element of NAT st k in dom r1 holds
r1 . k = (p . (k -' 1)) * (q . ((z + 1) -' k)) ) ) by POLYNOM3:def 9;
1 <= z + 1 by NAT_1:11;
then A1: 1 in dom r1 by FINSEQ_3:25, R;

now :: thesis: not z < (min* cp) + (min* cq)

assume AA1: z < (min* cp) + (min* cq) ; :: thesis: contradiction
F: for k being Nat holds
( not k in dom r1 or p . (k -' 1) = 0. R or q . ((z + 1) -' k) = 0. R )

proof

let k be Nat; :: thesis: ( not k in dom r1 or p . (k -' 1) = 0. R or q . ((z + 1) -' k) = 0. R )
assume k in dom r1 ; :: thesis: ( p . (k -' 1) = 0. R or q . ((z + 1) -' k) = 0. R )
then EF: ( 1 <= k & k <= len r1 ) by FINSEQ_3:25;

per cases ( k -' 1 >= min* cp or k -' 1 < min* cp ) ;

suppose AA0: k -' 1 >= min* cp ; :: thesis: ( p . (k -' 1) = 0. R or q . ((z + 1) -' k) = 0. R )

AA2: k -' 1 = k - 1 by EF, XREAL_0:def 2;
(z + 1) - k in NAT by INT_1:5, R, EF;
then (z + 1) -' k = (z + 1) - k by XREAL_0:def 2;
then (k -' 1) + ((z + 1) -' k) < (min* cp) + (min* cq) by AA1, AA2;
then S: (z + 1) -' k < min* cq by AA0, XREAL_1:7;

now :: thesis: not q . ((z + 1) -' k) <> 0. R

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

end;

hence ( p . (k -' 1) = 0. R or q . ((z + 1) -' k) = 0. R ) ; :: thesis: verum

end;

suppose S: k -' 1 < min* cp ; :: thesis: ( p . (k -' 1) = 0. R or q . ((z + 1) -' k) = 0. R )

now :: thesis: not p . (k -' 1) <> 0. R

assume p . (k -' 1) <> 0. R ; :: thesis: contradiction
then k -' 1 in cp ;
hence contradiction by S, NAT_1:def 1; :: thesis: verum

end;

hence ( p . (k -' 1) = 0. R or q . ((z + 1) -' k) = 0. R ) ; :: thesis: verum

end;

end;

end;

now :: thesis: for k being Element of NAT st k in dom r1 & k <> 1 holds
r1 /. k = 0. R

let k be Element of NAT ; :: thesis: ( k in dom r1 & k <> 1 implies r1 /. b₁ = 0. R )
assume E: ( k in dom r1 & k <> 1 ) ; :: thesis: r1 /. b₁ = 0. R

per cases ( p . (k -' 1) = 0. R or q . ((z + 1) -' k) = 0. R ) by F, E;

suppose p . (k -' 1) = 0. R ; :: thesis: r1 /. b₁ = 0. R

then r1 . k = (0. R) * (q . ((z + 1) -' k)) by E, R;
hence r1 /. k = 0. R by E, PARTFUN1:def 6; :: thesis: verum

end;

suppose q . ((z + 1) -' k) = 0. R ; :: thesis: r1 /. b₁ = 0. R

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

end;

end;

end;

then T: Sum r1 = r1 /. 1 by A1, POLYNOM2:3
.= r1 . 1 by A1, PARTFUN1:def 6
.= (p . (1 -' 1)) * (q . ((z + 1) -' 1)) by A1, R ;

now :: thesis: Sum r1 = 0. R

per cases ( p . (1 -' 1) = 0. R or q . ((z + 1) -' 1) = 0. R ) by A1, F;

suppose p . (1 -' 1) = 0. R ; :: thesis: Sum r1 = 0. R

hence Sum r1 = 0. R by T; :: thesis: verum

end;

suppose q . ((z + 1) -' 1) = 0. R ; :: thesis: Sum r1 = 0. R

hence Sum r1 = 0. R by T; :: thesis: verum

end;

end;

end;

hence contradiction by H1, R; :: thesis: verum

end;

hence z1 >= (min* cp) + (min* cq) ; :: thesis: verum

end;

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 A; :: thesis: verum