let x, y, x1 be Nat; :: thesis: ( x1 = 0 implies ( y = Product (1 + (x1 * (idseq x))) iff y = 1 ) )
assume A1: x1 = 0 ; :: thesis: ( y = Product (1 + (x1 * (idseq x))) iff y = 1 )
A2: len (idseq x) = x ;
rng (idseq x) c= REAL ;
then idseq x is FinSequence of REAL by FINSEQ_1:def 4;
then idseq x is Element of x -tuples_on REAL by A2, FINSEQ_2:92;
then x1 * (idseq x) = x |-> 0 by A1, RVSUM_1:53;
then 1 + (x1 * (idseq x)) = x |-> (1 + 0) by Th21;
hence ( y = Product (1 + (x1 * (idseq x))) iff y = 1 ) by RVSUM_1:102; :: thesis: verum