let i be Nat; :: thesis: Product (i |-> 1) = 1
Product (i |-> (the_unity_wrt multreal )) = the_unity_wrt multreal by SETWOP_2:35;
hence Product (i |-> 1) = 1 by BINOP_2:7; :: thesis: verum