set X = (Seg 1) --> REAL;
set E = CarProd ((Seg 1) --> REAL);
thus CarProd ((Seg 1) --> REAL) is Function of REAL,(REAL 1) by Th37, SRINGS_5:8; :: thesis: for s being object st s in REAL holds
(CarProd ((Seg 1) --> REAL)) . s = <*s*>
thus for s being object st s in REAL holds
(CarProd ((Seg 1) --> REAL)) . s = <*s*> :: thesis: verum

proof

let s be object ; :: thesis: ( s in REAL implies (CarProd ((Seg 1) --> REAL)) . s = <*s*> )
assume A1: s in REAL ; :: thesis: (CarProd ((Seg 1) --> REAL)) . s = <*s*>
A2: ex id1 being Function of (CarProduct (SubFin (((Seg 1) --> REAL),1))),(product (SubFin (((Seg 1) --> REAL),1))) st
( (Pt2FinSeq ((Seg 1) --> REAL)) . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (((Seg 1) --> REAL),1)) holds
id1 . x = <*x*> ) ) by Def5;
SubFin (((Seg 1) --> REAL),1) = ((Seg 1) --> REAL) | 1 by MEASUR13:def 5;
hence (CarProd ((Seg 1) --> REAL)) . s = <*s*> by A1, A2, Th37; :: thesis: verum

end;