set Y = (Seg 2) --> REAL;
set Y1 = SubFin (((Seg 2) --> REAL),1);
set F = CarProd ((Seg 2) --> REAL);
thus CarProd ((Seg 2) --> REAL) is Function of [:REAL,REAL:],(REAL 2) by Th37, SRINGS_5:8; :: thesis: for s, t being object st s in REAL & t in REAL holds
(CarProd ((Seg 2) --> REAL)) . [s,t] = <*s,t*>
thus for s, t being object st s in REAL & t in REAL holds
(CarProd ((Seg 2) --> REAL)) . [s,t] = <*s,t*> :: thesis: verum

proof

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

end;