for n being Nat holds product (ProductREAL n) = REAL n by Th7;