let F be non empty FinSequence of the carrier of (Polynom-Ring INT.Ring); :: thesis: for x being Element of F_Real holds eval ((~ (^ (Product F))),x) = Product (eval ((^ F),x))
let x be Element of F_Real; :: thesis: eval ((~ (^ (Product F))),x) = Product (eval ((^ F),x))
A1: Seg (len F) = dom F by FINSEQ_1:def 3
.= dom (^ F) by Def7
.= Seg (len (^ F)) by FINSEQ_1:def 3 ;
reconsider F2 = ^ F as non empty FinSequence of the carrier of (Polynom-Ring F_Real) by A1;
eval ((~ (^ (Product F))),x) = eval ((~ (Product F2)),x) by Lm38
.= Product (eval (F2,x)) by Th39 ;
hence eval ((~ (^ (Product F))),x) = Product (eval ((^ F),x)) ; :: thesis: verum