theorem Th38: :: MEASUR14:38

( CarProd ((Seg 1) --> REAL) is Function of REAL,(REAL 1) & ( for s being object st s in REAL holds
(CarProd ((Seg 1) --> REAL)) . s = <*s*> ) )