set X = (Seg 1) --> REAL;
1 in Seg 1 ;
then ((Seg 1) --> REAL) . 1 = REAL by FUNCOP_1:7;
hence ( CarProduct ((Seg 1) --> REAL) = REAL & ElmFin (((Seg 1) --> REAL),1) = REAL ) by MEASUR13:def 3, MEASUR13:def 1; :: thesis: ( CarProduct ((Seg 2) --> REAL) = [:REAL,REAL:] & ElmFin (((Seg 2) --> REAL),2) = REAL & CarProduct ((Seg 3) --> REAL) = [:REAL,REAL,REAL:] )
set Y = (Seg 2) --> REAL;
A1: ( 1 in Seg 2 & 2 in Seg 2 ) ;
then A2: ( ((Seg 2) --> REAL) . 1 = REAL & ((Seg 2) --> REAL) . 2 = REAL ) by FUNCOP_1:7;
CarProduct ((Seg 2) --> REAL) = [:((ProdFinSeq ((Seg 2) --> REAL)) . 1),(((Seg 2) --> REAL) . (1 + 1)):] by MEASUR13:def 3;
hence CarProduct ((Seg 2) --> REAL) = [:REAL,REAL:] by A2, MEASUR13:def 3; :: thesis: ( ElmFin (((Seg 2) --> REAL),2) = REAL & CarProduct ((Seg 3) --> REAL) = [:REAL,REAL,REAL:] )
ElmFin (((Seg 2) --> REAL),2) = ((Seg 2) --> REAL) . 2 by MEASUR13:def 1;
hence ElmFin (((Seg 2) --> REAL),2) = REAL by A1, FUNCOP_1:7; :: thesis: CarProduct ((Seg 3) --> REAL) = [:REAL,REAL,REAL:]
set Z = (Seg 3) --> REAL;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) ;
then A3: ( ((Seg 3) --> REAL) . 1 = REAL & ((Seg 3) --> REAL) . 2 = REAL & ((Seg 3) --> REAL) . 3 = REAL ) by FUNCOP_1:7;
( (ProdFinSeq ((Seg 3) --> REAL)) . 1 = ((Seg 3) --> REAL) . 1 & (ProdFinSeq ((Seg 3) --> REAL)) . 2 = [:((ProdFinSeq ((Seg 3) --> REAL)) . 1),(((Seg 3) --> REAL) . (1 + 1)):] & (ProdFinSeq ((Seg 3) --> REAL)) . 3 = [:((ProdFinSeq ((Seg 3) --> REAL)) . 2),(((Seg 3) --> REAL) . (2 + 1)):] ) by MEASUR13:def 3;
hence CarProduct ((Seg 3) --> REAL) = [:REAL,REAL,REAL:] by A3, ZFMISC_1:def 3; :: thesis: verum