let L be non degenerated domRing-like Ring; :: thesis: for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence holds deg (~ (Product (rpoly (f,z)))) = Sum f
let z be FinSequence of the carrier of L; :: thesis: for f being NAT -valued FinSequence holds deg (~ (Product (rpoly (f,z)))) = Sum f
let f be NAT -valued FinSequence; :: thesis: deg (~ (Product (rpoly (f,z)))) = Sum f
defpred S₁[ Nat] means ( $1 <= len f implies ( ~ (Product (rpoly ((f | $1),z))) <> 0_. L & deg (~ (Product (rpoly ((f | $1),z)))) = Sum (f | $1) ) );
( len (rpoly ((f | 0),z)) = len (f | 0) & len (f | 0) = 0 ) by Def1;
then rpoly ((f | 0),z) = <*> the carrier of (Polynom-Ring L) ;
then A1: Product (rpoly ((f | 0),z)) = 1_ (Polynom-Ring L) by GROUP_4:8;
len (1_. L) = 1 by POLYNOM4:4;
then A2: deg (1_. L) = 1 - 1 by HURWITZ:def 2;
A3: S₁[ 0 ] by A1, A2, POLYNOM3:37;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
A6: ~ (Product <*(@ (rpoly ((f /. (i + 1)),(z /. (i + 1)))))*>) = rpoly ((f /. (i + 1)),(z /. (i + 1))) by GROUP_4:9;
assume A7: i + 1 <= len f ; :: thesis: ( ~ (Product (rpoly ((f | (i + 1)),z))) <> 0_. L & deg (~ (Product (rpoly ((f | (i + 1)),z)))) = Sum (f | (i + 1)) )
A8: rpoly ((f | (i + 1)),z) = (rpoly ((f | i),z)) ^ <*(@ (rpoly ((f /. (i + 1)),(z /. (i + 1)))))*> by Th46, A7, NAT_1:13;
A9: ~ (Product (rpoly ((f | (i + 1)),z))) = (Product (rpoly ((f | i),z))) * (Product <*(@ (rpoly ((f /. (i + 1)),(z /. (i + 1)))))*>) by A8, GROUP_4:5
.= (~ (Product (rpoly ((f | i),z)))) *' (rpoly ((f /. (i + 1)),(z /. (i + 1)))) by A6, POLYNOM3:def 10 ;
then A10: deg (~ (Product (rpoly ((f | (i + 1)),z)))) = (deg (~ (Product (rpoly ((f | i),z))))) + (deg (rpoly ((f /. (i + 1)),(z /. (i + 1))))) by A5, A7, NAT_1:13, HURWITZ:23;
A11: i + 1 in dom f by A7, FINSEQ_3:25, NAT_1:11;
then A12: f | (i + 1) = (f | i) ^ <*(f . (i + 1))*> by FINSEQ_5:10;
( deg (rpoly ((f /. (i + 1)),(z /. (i + 1)))) = f /. (i + 1) & f /. (i + 1) = f . (i + 1) ) by A11, HURWITZ:27, PARTFUN1:def 6;
hence ( ~ (Product (rpoly ((f | (i + 1)),z))) <> 0_. L & deg (~ (Product (rpoly ((f | (i + 1)),z)))) = Sum (f | (i + 1)) ) by A9, UPROOTS:21, A7, NAT_1:13, A5, A12, A10, RVSUM_1:74; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
then S₁[ len f] ;
hence deg (~ (Product (rpoly (f,z)))) = Sum f ; :: thesis: verum