theorem Th25: :: EUCLID_9:25

for n being Nat holds Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1))