theorem Th13: :: MESFUN18:13

( CarProduct ((Seg 1) --> RNS_Real) = RNS_Real & ElmFin (((Seg 1) --> RNS_Real),1) = RNS_Real & 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:] )