set Z = (Seg 3) --> REAL;
set Z2 = SubFin (((Seg 3) --> REAL),2);
set H = CarProd ((Seg 3) --> REAL);
thus CarProd ((Seg 3) --> REAL) is Function of [:REAL,REAL,REAL:],(REAL 3) by Th37, SRINGS_5:8; :: thesis: 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*>
thus 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*> :: thesis: verum

proof

let s, t, u be object ; :: thesis: ( s in REAL & t in REAL & u in REAL implies (CarProd ((Seg 3) --> REAL)) . [[s,t],u] = <*s,t,u*> )
assume A1: ( s in REAL & t in REAL & u in REAL ) ; :: thesis: (CarProd ((Seg 3) --> REAL)) . [[s,t],u] = <*s,t,u*>
A2: ( 1 in Seg 2 & 2 in Seg 2 & 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) ;
A3: len (SubFin (((Seg 3) --> REAL),2)) = 2 by CARD_1:def 7;
A4: SubFin (((Seg 3) --> REAL),2) = ((Seg 3) --> REAL) | 2 by MEASUR13:def 5;
then (SubFin (((Seg 3) --> REAL),2)) . 2 = ((Seg 3) --> REAL) . 2 by A2, FUNCT_1:49;
then A5: (SubFin (((Seg 3) --> REAL),2)) . 2 = REAL by A2, FUNCOP_1:7;
(SubFin (((Seg 3) --> REAL),2)) . 1 = ((Seg 3) --> REAL) . 1 by A4, A2, FUNCT_1:49;
then SubFin (((Seg 3) --> REAL),2) = <*REAL,REAL*> by A5, A3, A2, FUNCOP_1:7, FINSEQ_1:44;
then A6: SubFin (((Seg 3) --> REAL),2) = 2 |-> REAL by FINSEQ_2:61;
then A7: (CarProd (SubFin (((Seg 3) --> REAL),2))) . [s,t] = <*s,t*> by A1, Th39;
ElmFin (((Seg 3) --> REAL),3) = ((Seg 3) --> REAL) . 3 by MEASUR13:def 1;
then ElmFin (((Seg 3) --> REAL),(2 + 1)) = REAL by A2, FUNCOP_1:7;
then ex a, b being FinSequence st
( (CarProd (SubFin (((Seg 3) --> REAL),2))) . [s,t] = a & <*u*> = b & (CarProd ((Seg 3) --> REAL)) . ([s,t],u) = a ^ b ) by A1, A6, Th37, Th13, ZFMISC_1:87;
hence (CarProd ((Seg 3) --> REAL)) . [[s,t],u] = <*s,t,u*> by A7; :: thesis: verum

end;