theorem Th39: :: MEASUR14:39

( CarProd ((Seg 2) --> REAL) is Function of [:REAL,REAL:],(REAL 2) & ( for s, t being object st s in REAL & t in REAL holds
(CarProd ((Seg 2) --> REAL)) . [s,t] = <*s,t*> ) )