let L be non degenerated comRing; :: thesis: for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for x being Element of the carrier of L ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly (f,z)))),x) = Product e & len e = len f & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )
let z be FinSequence of the carrier of L; :: thesis: for f being NAT -valued FinSequence
for x being Element of the carrier of L ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly (f,z)))),x) = Product e & len e = len f & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )
let f be NAT -valued FinSequence; :: thesis: for x being Element of the carrier of L ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly (f,z)))),x) = Product e & len e = len f & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )
let x be Element of the carrier of L; :: thesis: ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly (f,z)))),x) = Product e & len e = len f & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )
defpred S₁[ Nat] means ( $1 <= len f implies ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly ((f | $1),z)))),x) = Product e & len e = $1 & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) ) );
A1: S₁[ 0 ]

proof

assume 0 <= len f ; :: thesis: ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly ((f | 0),z)))),x) = Product e & len e = 0 & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )
take e = <*> the carrier of L; :: thesis: ( eval ((~ (Product (rpoly ((f | 0),z)))),x) = Product e & len e = 0 & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )
( 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 Product (rpoly ((f | 0),z)) = 1_ (Polynom-Ring L) by GROUP_4:8;
then ~ (Product (rpoly ((f | 0),z))) = 1_. L by POLYNOM3:37;
then eval ((~ (Product (rpoly ((f | 0),z)))),x) = 1_ L by POLYNOM4:18;
then eval ((~ (Product (rpoly ((f | 0),z)))),x) = Product e by GROUP_4:8;
hence ( eval ((~ (Product (rpoly ((f | 0),z)))),x) = Product e & len e = 0 & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) ) ; :: thesis: verum

end;

A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
assume A4: i + 1 <= len f ; :: thesis: ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly ((f | (i + 1)),z)))),x) = Product e & len e = i + 1 & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )
then consider e being FinSequence of the carrier of L such that
A5: eval ((~ (Product (rpoly ((f | i),z)))),x) = Product e and
A6: len e = i and
A7: for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) by A3, NAT_1:13;
set E = eval ((rpoly ((f /. (i + 1)),(z /. (i + 1)))),x);
take e1 = e ^ <*(eval ((rpoly ((f /. (i + 1)),(z /. (i + 1)))),x))*>; :: thesis: ( eval ((~ (Product (rpoly ((f | (i + 1)),z)))),x) = Product e1 & len e1 = i + 1 & ( for i being Nat st 1 <= i & i <= len e1 holds
e1 . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )
A8: ~ (Product <*(@ (rpoly ((f /. (i + 1)),(z /. (i + 1)))))*>) = rpoly ((f /. (i + 1)),(z /. (i + 1))) by GROUP_4:9;
A9: rpoly ((f | (i + 1)),z) = (rpoly ((f | i),z)) ^ <*(@ (rpoly ((f /. (i + 1)),(z /. (i + 1)))))*> by A4, Th46, NAT_1:13;
~ (Product (rpoly ((f | (i + 1)),z))) = (Product (rpoly ((f | i),z))) * (Product <*(@ (rpoly ((f /. (i + 1)),(z /. (i + 1)))))*>) by A9, GROUP_4:5
.= (~ (Product (rpoly ((f | i),z)))) *' (rpoly ((f /. (i + 1)),(z /. (i + 1)))) by A8, POLYNOM3:def 10 ;
hence eval ((~ (Product (rpoly ((f | (i + 1)),z)))),x) = (Product e) * (eval ((rpoly ((f /. (i + 1)),(z /. (i + 1)))),x)) by A5, POLYNOM4:24
.= Product e1 by GROUP_4:6 ;
:: thesis: ( len e1 = i + 1 & ( for i being Nat st 1 <= i & i <= len e1 holds
e1 . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )
thus A10: len e1 = i + 1 by A6, FINSEQ_2:16; :: thesis: for i being Nat st 1 <= i & i <= len e1 holds
e1 . i = eval ((rpoly ((f /. i),(z /. i))),x)
let j be Nat; :: thesis: ( 1 <= j & j <= len e1 implies e1 . j = eval ((rpoly ((f /. j),(z /. j))),x) )
assume A11: ( 1 <= j & j <= len e1 ) ; :: thesis: e1 . j = eval ((rpoly ((f /. j),(z /. j))),x)

per cases ( j = len e1 or j < len e1 ) by A11, XXREAL_0:1;

suppose j = len e1 ; :: thesis: e1 . j = eval ((rpoly ((f /. j),(z /. j))),x)

hence e1 . j = eval ((rpoly ((f /. j),(z /. j))),x) by A10, A6; :: thesis: verum

end;

suppose j < len e1 ; :: thesis: e1 . j = eval ((rpoly ((f /. j),(z /. j))),x)

then A12: j <= i by A10, NAT_1:13;
then j in dom e by A11, A6, FINSEQ_3:25;
then e1 . j = e . j by FINSEQ_1:def 7;
hence e1 . j = eval ((rpoly ((f /. j),(z /. j))),x) by A12, A11, A6, A7; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
then S₁[ len f] ;
hence ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly (f,z)))),x) = Product e & len e = len f & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) ) ; :: thesis: verum