let i be natural Number ; :: thesis: Product (i |-> 1) = 1
i is Nat by TARSKI:1;
then Product (i |-> (the_unity_wrt multreal)) = the_unity_wrt multreal by SETWOP_2:25;
hence Product (i |-> 1) = 1 by BINOP_2:7; :: thesis: verum