let i be Nat; :: thesis: Product (i |-> 1) = 1
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