theorem :: MEASUR14:40

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