set X = (Seg 1) --> RNS_Real;
1 in Seg 1
;
then
((Seg 1) --> RNS_Real) . 1 = RNS_Real
by FUNCOP_1:7;
hence
( CarProduct ((Seg 1) --> RNS_Real) = RNS_Real & ElmFin (((Seg 1) --> RNS_Real),1) = RNS_Real )
by MEASUR15:def 3, MEASUR15:def 4; ( CarProduct ((Seg 2) --> RNS_Real) = [:RNS_Real,RNS_Real:] & ElmFin (((Seg 2) --> RNS_Real),2) = RNS_Real & CarProduct ((Seg 3) --> RNS_Real) = [:RNS_Real,RNS_Real,RNS_Real:] )
set Y = (Seg 2) --> RNS_Real;
A1:
( 1 in Seg 2 & 2 in Seg 2 )
;
then A2:
( ((Seg 2) --> RNS_Real) . 1 = RNS_Real & ((Seg 2) --> RNS_Real) . 2 = RNS_Real )
by FUNCOP_1:7;
CarProduct (SubFin (((Seg 2) --> RNS_Real),1)) = (ProdFinSeq ((Seg 2) --> RNS_Real)) . 1
by MEASUR15:9;
then A3:
CarProduct (SubFin (((Seg 2) --> RNS_Real),1)) = RNS_Real
by A2, MEASUR15:def 4;
ElmFin (((Seg 2) --> RNS_Real),(1 + 1)) = RNS_Real
by A2, MEASUR15:def 3;
hence
CarProduct ((Seg 2) --> RNS_Real) = [:RNS_Real,RNS_Real:]
by A3, MEASUR15:10; ( ElmFin (((Seg 2) --> RNS_Real),2) = RNS_Real & CarProduct ((Seg 3) --> RNS_Real) = [:RNS_Real,RNS_Real,RNS_Real:] )
ElmFin (((Seg 2) --> RNS_Real),2) = ((Seg 2) --> RNS_Real) . 2
by MEASUR15:def 3;
hence
ElmFin (((Seg 2) --> RNS_Real),2) = RNS_Real
by A1, FUNCOP_1:7; CarProduct ((Seg 3) --> RNS_Real) = [:RNS_Real,RNS_Real,RNS_Real:]
set Z = (Seg 3) --> RNS_Real;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 )
;
then A4:
( ((Seg 3) --> RNS_Real) . 1 = RNS_Real & ((Seg 3) --> RNS_Real) . 2 = RNS_Real & ((Seg 3) --> RNS_Real) . 3 = RNS_Real )
by FUNCOP_1:7;
then A5:
(ProdFinSeq ((Seg 3) --> RNS_Real)) . 1 = RNS_Real
by MEASUR15:def 4;
A6:
ex Z21, Z22 being RealNormSpace st
( Z21 = (ProdFinSeq ((Seg 3) --> RNS_Real)) . 1 & Z22 = ((Seg 3) --> RNS_Real) . (1 + 1) & (ProdFinSeq ((Seg 3) --> RNS_Real)) . 2 = [:Z21,Z22:] )
by MEASUR15:def 4;
A7:
CarProduct ((Seg 3) --> RNS_Real) = [:(CarProduct (SubFin (((Seg 3) --> RNS_Real),2))),(ElmFin (((Seg 3) --> RNS_Real),(2 + 1))):]
by MEASUR15:10;
A8:
CarProduct (SubFin (((Seg 3) --> RNS_Real),2)) = [:RNS_Real,RNS_Real:]
by A4, A5, A6, MEASUR15:9;
ElmFin (((Seg 3) --> RNS_Real),3) = RNS_Real
by A4, MEASUR15:def 3;
hence
CarProduct ((Seg 3) --> RNS_Real) = [:RNS_Real,RNS_Real,RNS_Real:]
by A7, A8, PRVECT_4:def 3; verum