:: Measure for Product Space of Real Normed Spaces
:: by Noboru Endou and Yasunari Shidama
::
:: Received December 2, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

Lm9: for x, a being Real ex r being Real st
( 0 < r & x in ].(a - r),(a + r).[ )

proof end;

Lm1: for G being RealLinearSpace-Sequence
for v, w being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:(addop G):] . (v,w)) . i = the addF of (G . i) . ((v . i),(w . i)) & ( for vi, wi being VECTOR of (G . i) st vi = v . i & wi = w . i holds
([:(addop G):] . (v,w)) . i = vi + wi ) )

proof end;

Lm2: for G being RealLinearSpace-Sequence
for r being Element of REAL
for v being Element of product (carr G)
for i being Element of dom (carr G) holds
( ([:(multop G):] . (r,v)) . i = the Mult of (G . i) . (r,(v . i)) & ( for vi being VECTOR of (G . i) st vi = v . i holds
([:(multop G):] . (r,v)) . i = r * vi ) )

proof end;

theorem :: MEASUR15:1

for G being RealLinearSpace-Sequence
for v, w, s being Element of (product G)
for v1, w1, s1 being Element of product (carr G) st v = v1 & w = w1 & s = s1 holds
( s = v + w iff for i being Element of dom (carr G)
for vi, wi being VECTOR of (G . i) st vi = v1 . i & wi = w1 . i holds
s1 . i = vi + wi )

proof end;

theorem :: MEASUR15:2

for G being RealLinearSpace-Sequence
for r being Element of REAL
for v, w being Element of (product G)
for v1, w1 being Element of product (carr G) st v = v1 & w = w1 holds
( w = r * v iff for i being Element of dom (carr G)
for vi being VECTOR of (G . i) st vi = v1 . i holds
w1 . i = r * vi )

proof end;

Lm3: for x being Element of REAL 1
for r being Real st x = <*r*> holds
|.x.| = |.r.|

proof end;

Lm4: for p, q, w being FinSequence of REAL
for r being Element of REAL st w = <*|.p.|,r*> & q = p ^ <*r*> holds
|.w.| = |.q.|

proof end;

definition

let n be non zero Nat;
let p be n -element FinSequence;

func PtProdFinSeq p -> n -element FinSequence means :Def1: :: MEASUR15:def 1
( it . 1 = p . 1 & ( for i being non zero Nat st i < n holds
it . (i + 1) = [(it . i),(p . (i + 1))] ) );

existence
ex b₁ being n -element FinSequence st
( b₁ . 1 = p . 1 & ( for i being non zero Nat st i < n holds
b₁ . (i + 1) = [(b₁ . i),(p . (i + 1))] ) )

proof end;

uniqueness
for b₁, b₂ being n -element FinSequence st b₁ . 1 = p . 1 & ( for i being non zero Nat st i < n holds
b₁ . (i + 1) = [(b₁ . i),(p . (i + 1))] ) & b₂ . 1 = p . 1 & ( for i being non zero Nat st i < n holds
b₂ . (i + 1) = [(b₂ . i),(p . (i + 1))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines PtProdFinSeq MEASUR15:def 1 :
for n being non zero Nat
for p, b₃ being b₁ -element FinSequence holds
( b₃ = PtProdFinSeq p iff ( b₃ . 1 = p . 1 & ( for i being non zero Nat st i < n holds
b₃ . (i + 1) = [(b₃ . i),(p . (i + 1))] ) ) );

definition

let n be non zero Nat;
let p be n -element FinSequence;

func PtCarProduct p -> set equals :: MEASUR15:def 2
(PtProdFinSeq p) . n;

coherence
(PtProdFinSeq p) . n is set ;

end;

:: deftheorem defines PtCarProduct MEASUR15:def 2 :
for n being non zero Nat
for p being b₁ -element FinSequence holds PtCarProduct p = (PtProdFinSeq p) . n;

theorem Th3: :: MEASUR15:3

for n, m being non zero Nat
for p being b₁ -element FinSequence
for q being b₂ -element FinSequence st m <= n & q = p | m holds
PtProdFinSeq q = (PtProdFinSeq p) | m

proof end;

theorem Th4: :: MEASUR15:4

for n being non zero Nat
for p being b₁ + 1 -element FinSequence
for q being b₁ -element FinSequence st q = p | n holds
PtCarProduct p = [(PtCarProduct q),(p . (n + 1))]

proof end;

theorem Th5: :: MEASUR15:5

for n being non zero Nat
for p1, p2 being b₁ -element FinSequence holds
( PtCarProduct p1 = PtCarProduct p2 iff p1 = p2 )

proof end;

theorem Th6: :: MEASUR15:6

for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for x being object holds
( x in CarProduct X iff ex px being b₁ -element FinSequence st
( px in product X & x = PtCarProduct px ) )

proof end;

registration

let n be non empty Nat;

cluster Relation-like omega -defined Function-like non empty finite n -element countable FinSequence-like FinSubsequence-like 1-sorted-yielding non-Empty non-empty-addLoopStr-yielding RealLinearSpace-yielding RealNormSpace-yielding for set ;

correctness
existence
ex b₁ being RealNormSpace-Sequence st b₁ is n -element ;

proof end;

end;

definition

let m, n be non zero Nat;
let X be n -element RealNormSpace-Sequence;
assume A1: m <= n ;

func ElmFin (X,m) -> RealNormSpace equals :Def3: :: MEASUR15:def 3
X . m;

coherence
X . m is RealNormSpace

proof end;

end;

:: deftheorem Def3 defines ElmFin MEASUR15:def 3 :
for m, n being non zero Nat
for X being b₂ -element RealNormSpace-Sequence st m <= n holds
ElmFin (X,m) = X . m;

definition

let n be non zero Nat;
let X be n -element RealNormSpace-Sequence;

func ProdFinSeq X -> n -element RealNormSpace-Sequence means :Def4: :: MEASUR15:def 4
( it . 1 = X . 1 & ( for i being non zero Nat st i < n holds
ex X1, X2 being RealNormSpace st
( X1 = it . i & X2 = X . (i + 1) & it . (i + 1) = [:X1,X2:] ) ) );

existence
ex b₁ being n -element RealNormSpace-Sequence st
( b₁ . 1 = X . 1 & ( for i being non zero Nat st i < n holds
ex X1, X2 being RealNormSpace st
( X1 = b₁ . i & X2 = X . (i + 1) & b₁ . (i + 1) = [:X1,X2:] ) ) )

proof end;

uniqueness
for b₁, b₂ being n -element RealNormSpace-Sequence st b₁ . 1 = X . 1 & ( for i being non zero Nat st i < n holds
ex X1, X2 being RealNormSpace st
( X1 = b₁ . i & X2 = X . (i + 1) & b₁ . (i + 1) = [:X1,X2:] ) ) & b₂ . 1 = X . 1 & ( for i being non zero Nat st i < n holds
ex X1, X2 being RealNormSpace st
( X1 = b₂ . i & X2 = X . (i + 1) & b₂ . (i + 1) = [:X1,X2:] ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines ProdFinSeq MEASUR15:def 4 :
for n being non zero Nat
for X, b₃ being b₁ -element RealNormSpace-Sequence holds
( b₃ = ProdFinSeq X iff ( b₃ . 1 = X . 1 & ( for i being non zero Nat st i < n holds
ex X1, X2 being RealNormSpace st
( X1 = b₃ . i & X2 = X . (i + 1) & b₃ . (i + 1) = [:X1,X2:] ) ) ) );

definition

let n be non zero Nat;
let X be n -element RealNormSpace-Sequence;

func CarProduct X -> RealNormSpace equals :: MEASUR15:def 5
(ProdFinSeq X) . n;

coherence
(ProdFinSeq X) . n is RealNormSpace

proof end;

end;

:: deftheorem defines CarProduct MEASUR15:def 5 :
for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence holds CarProduct X = (ProdFinSeq X) . n;

registration

let n be non zero Nat;
let X be n -element RealNormSpace-Sequence;

cluster CarProduct X -> ;

coherence
not CarProduct X is empty ;

end;

theorem Th7: :: MEASUR15:7

for m, n being non zero Nat
for X being b₂ -element RealNormSpace-Sequence st m <= n holds
X | m is b₁ -element RealNormSpace-Sequence

proof end;

definition

let m, n be non zero Nat;
let X be n -element RealNormSpace-Sequence;
assume A1: m <= n ;

func SubFin (X,m) -> m -element RealNormSpace-Sequence equals :Def6: :: MEASUR15:def 6
X | m;

correctness
coherence
X | m is m -element RealNormSpace-Sequence;
by A1, Th7;

end;

:: deftheorem Def6 defines SubFin MEASUR15:def 6 :
for m, n being non zero Nat
for X being b₂ -element RealNormSpace-Sequence st m <= n holds
SubFin (X,m) = X | m;

theorem Th8: :: MEASUR15:8

for i, j, k, n being non zero Nat
for X being b₄ -element RealNormSpace-Sequence st i <= j & j <= k & k <= n holds
(ProdFinSeq (SubFin (X,j))) . i = (ProdFinSeq (SubFin (X,k))) . i

proof end;

theorem Th9: :: MEASUR15:9

for m, n being non zero Nat
for X being b₂ -element RealNormSpace-Sequence st m <= n holds
(ProdFinSeq X) . m = (ProdFinSeq (SubFin (X,m))) . m

proof end;

theorem Th10: :: MEASUR15:10

for n being non zero Nat
for X being b₁ + 1 -element RealNormSpace-Sequence holds CarProduct X = [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):]

proof end;

theorem Th11: :: MEASUR15:11

for k, m, n being non zero Nat
for X being b₃ -element RealNormSpace-Sequence st k <= m & m <= n holds
SubFin (X,k) = SubFin ((SubFin (X,m)),k)

proof end;

Lm5: for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence ex CX being non-empty b₁ -element FinSequence st
( CarProduct CX = the carrier of (CarProduct X) & ( for i being non zero Nat st i <= n holds
CX . i = the carrier of (ElmFin (X,i)) ) )

proof end;

theorem Th12: :: MEASUR15:12

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence ex CX being non-empty b₁ -element FinSequence st
( CarProduct CX = the carrier of (CarProduct X) & CX = carr X & ( for i being non zero Nat st i <= n holds
CX . i = the carrier of (ElmFin (X,i)) ) )

proof end;

theorem Th13: :: MEASUR15:13

for k, m, n being non zero Nat
for X being b₃ -element RealNormSpace-Sequence st k <= m & m <= n holds
ElmFin (X,k) = ElmFin ((SubFin (X,m)),k)

proof end;

theorem :: MEASUR15:14

for m, n being non zero Nat
for X being b₂ -element RealNormSpace-Sequence st m < n holds
CarProduct (SubFin (X,(m + 1))) = [:(CarProduct (SubFin (X,m))),(ElmFin (X,(m + 1))):]

proof end;

theorem :: MEASUR15:15

for m, n being non zero Nat
for X being b₂ + 1 -element RealNormSpace-Sequence st m <= n holds
CarProduct (SubFin (X,m)) = CarProduct (SubFin ((SubFin (X,n)),m))

proof end;

theorem Th16: :: MEASUR15:16

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x being object holds
( x is Point of (CarProduct X) iff ex px being b₁ -element FinSequence st
( x = PtCarProduct px & ( for i being non zero Nat st i <= n holds
ex pxi being Point of (ElmFin (X,i)) st pxi = px . i ) ) )

proof end;

theorem Th17: :: MEASUR15:17

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x being Point of (CarProduct X)
for px being b₁ -element FinSequence st x = PtCarProduct px holds
for i being non zero Nat st i <= n holds
ex pxi being Point of (ElmFin (X,i)) st pxi = px . i

proof end;

theorem Th18: :: MEASUR15:18

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x, y being Point of (CarProduct X)
for px, py being b₁ -element FinSequence st x = PtCarProduct px & y = PtCarProduct py holds
ex pxy being b₁ -element FinSequence st x + y = PtCarProduct pxy

proof end;

theorem Th19: :: MEASUR15:19

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x, y, z being Point of (CarProduct X)
for px, py, pz being b₁ -element FinSequence st x = PtCarProduct px & y = PtCarProduct py & x + y = PtCarProduct pz holds
for i being non zero Nat st i <= n holds
ex pxi, pyi being Point of (ElmFin (X,i)) st
( pxi = px . i & pyi = py . i & pxi + pyi = pz . i )

proof end;

theorem Th20: :: MEASUR15:20

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for r being Real
for x being Point of (CarProduct X)
for px being b₁ -element FinSequence st x = PtCarProduct px holds
ex prx being b₁ -element FinSequence st r * x = PtCarProduct prx

proof end;

theorem Th21: :: MEASUR15:21

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for r being Real
for x being Point of (CarProduct X)
for px, prx being b₁ -element FinSequence st x = PtCarProduct px & r * x = PtCarProduct prx holds
for i being non zero Nat st i <= n holds
ex pxi being Point of (ElmFin (X,i)) st
( pxi = px . i & r * pxi = prx . i )

proof end;

theorem Th22: :: MEASUR15:22

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x being Point of (CarProduct X)
for px being b₁ -element FinSequence st x = PtCarProduct px holds
ex prx being b₁ -element FinSequence st - x = PtCarProduct prx

proof end;

theorem Th23: :: MEASUR15:23

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x being Point of (CarProduct X)
for px, pmx being b₁ -element FinSequence st x = PtCarProduct px & - x = PtCarProduct pmx holds
for i being non zero Nat st i <= n holds
ex pxi being Point of (ElmFin (X,i)) st
( pxi = px . i & - pxi = pmx . i )

proof end;

theorem Th24: :: MEASUR15:24

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x, y being Point of (CarProduct X)
for px, py being b₁ -element FinSequence st x = PtCarProduct px & y = PtCarProduct py holds
ex pxy being b₁ -element FinSequence st x - y = PtCarProduct pxy

proof end;

theorem Th25: :: MEASUR15:25

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x, y being Point of (CarProduct X)
for px, py, pxy being b₁ -element FinSequence st x = PtCarProduct px & y = PtCarProduct py & x - y = PtCarProduct pxy holds
for i being non zero Nat st i <= n holds
ex pxi, pyi being Point of (ElmFin (X,i)) st
( pxi = px . i & pyi = py . i & pxi - pyi = pxy . i )

proof end;

theorem Th26: :: MEASUR15:26

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x being Point of (CarProduct X)
for px being b₁ -element FinSequence st x = PtCarProduct px holds
ex nrx being Element of REAL n st
( ( for i being non zero Nat st i <= n holds
ex pxi being Point of (ElmFin (X,i)) st
( pxi = px . i & nrx . i = ||.pxi.|| ) ) & ||.x.|| = |.nrx.| )

proof end;

definition

let n be non zero Nat;
let X be n -element RealNormSpace-Sequence;

func CarProd X -> Function of (CarProduct X),(product X) means :Def7: :: MEASUR15:def 7
ex CX being non-empty n -element FinSequence st
( CX = carr X & CarProduct CX = the carrier of (CarProduct X) & it = CarProd CX & it is bijective );

existence
ex b₁ being Function of (CarProduct X),(product X) ex CX being non-empty n -element FinSequence st
( CX = carr X & CarProduct CX = the carrier of (CarProduct X) & b₁ = CarProd CX & b₁ is bijective )

proof end;

uniqueness
for b₁, b₂ being Function of (CarProduct X),(product X) st ex CX being non-empty n -element FinSequence st
( CX = carr X & CarProduct CX = the carrier of (CarProduct X) & b₁ = CarProd CX & b₁ is bijective ) & ex CX being non-empty n -element FinSequence st
( CX = carr X & CarProduct CX = the carrier of (CarProduct X) & b₂ = CarProd CX & b₂ is bijective ) holds
b₁ = b₂ ;

end;

:: deftheorem Def7 defines CarProd MEASUR15:def 7 :
for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for b₃ being Function of (CarProduct X),(product X) holds
( b₃ = CarProd X iff ex CX being non-empty b₁ -element FinSequence st
( CX = carr X & CarProduct CX = the carrier of (CarProduct X) & b₃ = CarProd CX & b₃ is bijective ) );

theorem Th27: :: MEASUR15:27

for n being non zero Nat
for X, X1 being RealNormSpace-Sequence st n <= len X & X1 = X | n holds
carr X1 = (carr X) | n

proof end;

theorem Th28: :: MEASUR15:28

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x being Point of (CarProduct X) ex px being b₁ -element FinSequence st
( x = PtCarProduct px & (CarProd X) . x = px )

proof end;

theorem Th29: :: MEASUR15:29

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x, y being Point of (CarProduct X) holds (CarProd X) . (x + y) = ((CarProd X) . x) + ((CarProd X) . y)

proof end;

theorem Th30: :: MEASUR15:30

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x being Point of (CarProduct X)
for r being Element of REAL holds (CarProd X) . (r * x) = r * ((CarProd X) . x)

proof end;

theorem Th31: :: MEASUR15:31

for n being non zero Nat
for X being b₁ -element RealNormSpace-Sequence
for x being Point of (CarProduct X) holds ||.((CarProd X) . x).|| = ||.x.||

proof end;

Lm6: for n being non zero Nat
for X being non empty set holds (Seg n) --> X is non-empty b₁ -element FinSequence

proof end;

registration

let n be non zero Nat;
let X be non empty set ;

cluster (Seg n) --> X -> non-empty n -element for FinSequence;

correctness
coherence
for b₁ being FinSequence st b₁ = (Seg n) --> X holds
( b₁ is non-empty & b₁ is n -element );
by Lm6;

end;

registration

let n be non zero Nat;

cluster (Seg n) --> RNS_Real -> non empty n -element RealNormSpace-yielding for FinSequence;

correctness
coherence
for b₁ being FinSequence st b₁ = (Seg n) --> RNS_Real holds
( b₁ is n -element & not b₁ is empty & b₁ is RealNormSpace-yielding );

proof end;

end;

theorem Th32: :: MEASUR15:32

for n being non zero Nat
for u being object holds
( u is Point of (CarProduct ((Seg n) --> RNS_Real)) iff ex pu being b₁ -element FinSequence of RNS_Real st u = PtCarProduct pu )

proof end;

Lm7: for n being non zero Nat
for a being b₁ -element FinSequence of REAL
for r being Real st 0 < r holds
ex D1 being non-empty b₁ -element FinSequence st
for i being Nat st i in Seg n holds
D1 . i = ].((a . i) - r),((a . i) + r).[

proof end;

theorem Th33: :: MEASUR15:33

for n being non zero Nat
for D being non-empty b₁ -element FinSequence
for px being b₁ -element FinSequence holds
( PtCarProduct px in CarProduct D iff for i being Nat st i in Seg n holds
px . i in D . i )

proof end;

theorem Th34: :: MEASUR15:34

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
D . i c= REAL ) holds
CarProduct D c= CarProduct ((Seg n) --> REAL)

proof end;

theorem Th35: :: MEASUR15:35

for n being non zero Nat holds CarProduct ((Seg n) --> RAT) is countable

proof end;

Lm8: for n being non zero Nat
for a being b₁ -element FinSequence of REAL
for r being Real st 0 < r holds
ex b being b₁ -element FinSequence of RAT st
for i being Nat st i in Seg n holds
b . i in ].((a . i) - r),((a . i) + r).[

proof end;

Lm10: for n being non zero Nat
for a, x being b₁ -element FinSequence of REAL ex r being Real st
( 0 < r & ( for i being Nat st i in Seg n holds
x . i in ].((a . i) - r),((a . i) + r).[ ) )

proof end;

theorem Th36: :: MEASUR15:36

for n being non zero Nat holds Prod_Measure (L-Meas n) is sigma_finite

proof end;

theorem :: MEASUR15:37

for n being non zero Nat holds Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) is sigma_finite

proof end;

theorem :: MEASUR15:38

for n being non zero Nat holds
( CarProduct ((Seg (n + 1)) --> REAL) = [:(CarProduct ((Seg n) --> REAL)),REAL:] & CarProduct ((Seg (n + 1)) --> RNS_Real) = [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] )

proof end;

theorem Th39: :: MEASUR15:39

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is Element of L-Field ) holds
CarProduct D is Element of Prod_Field (L-Field n)

proof end;

theorem Th40: :: MEASUR15:40

for n being non zero Nat holds CarProduct ((Seg n) --> REAL) in Prod_Field (L-Field n)

proof end;

theorem :: MEASUR15:41

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is Interval ) holds
CarProduct D is Element of Prod_Field (L-Field n)

proof end;

theorem Th42: :: MEASUR15:42

for n being non zero Nat holds the carrier of (CarProduct ((Seg n) --> RNS_Real)) = CarProduct ((Seg n) --> REAL)

proof end;

theorem Th43: :: MEASUR15:43

for n being non zero Nat
for px being b₁ -element FinSequence of REAL holds px in product ((Seg n) --> REAL)

proof end;

theorem Th44: :: MEASUR15:44

for n being non zero Nat
for px being b₁ -element FinSequence of RAT holds px in product ((Seg n) --> RAT)

proof end;

theorem Th45: :: MEASUR15:45

for n being non zero Nat
for x being object holds
( x in CarProduct ((Seg n) --> REAL) iff ex px being b₁ -element FinSequence of REAL st x = PtCarProduct px )

proof end;

theorem Th46: :: MEASUR15:46

for n being non zero Nat
for x being object holds
( x in CarProduct ((Seg n) --> RAT) iff ex px being b₁ -element FinSequence of RAT st x = PtCarProduct px )

proof end;

theorem :: MEASUR15:47

for n being non zero Nat
for x being object st x in CarProduct ((Seg n) --> REAL) holds
ex px being b₁ -element FinSequence of REAL st
( px in product ((Seg n) --> REAL) & x = PtCarProduct px )

proof end;

theorem Th48: :: MEASUR15:48

for n being non zero Nat
for X, Y being non-empty b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
X . i c= Y . i ) holds
CarProduct X c= CarProduct Y

proof end;

theorem Th49: :: MEASUR15:49

for n being non zero Nat holds CarProduct ((Seg n) --> RAT) c= CarProduct ((Seg n) --> REAL)

proof end;

theorem :: MEASUR15:50

for n being non zero Nat
for X being non empty set
for D being non-empty b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is Subset of X ) holds
CarProduct D is Subset of (CarProduct ((Seg n) --> X))

proof end;

theorem Th51: :: MEASUR15:51

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) holds
ex E being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( E = CarProduct D & E is compact )

proof end;

theorem :: MEASUR15:52

for n being non zero Nat
for x, y being Point of (CarProduct ((Seg n) --> RNS_Real))
for px, py being b₁ -element FinSequence of REAL st x = PtCarProduct px & y = PtCarProduct py holds
ex pxy being b₁ -element FinSequence of REAL st x + y = PtCarProduct pxy

proof end;

theorem :: MEASUR15:53

for n being non zero Nat
for x, y being Point of (CarProduct ((Seg n) --> RNS_Real))
for px, py, pxy being b₁ -element FinSequence of REAL st x = PtCarProduct px & y = PtCarProduct py & x + y = PtCarProduct pxy holds
for i being Nat st i in Seg n holds
pxy . i = (px . i) + (py . i)

proof end;

theorem Th54: :: MEASUR15:54

for n being non zero Nat
for x, y being Point of (CarProduct ((Seg n) --> RNS_Real))
for px, py being b₁ -element FinSequence of REAL st x = PtCarProduct px & y = PtCarProduct py holds
ex pxy being b₁ -element FinSequence of REAL st x - y = PtCarProduct pxy

proof end;

theorem Th55: :: MEASUR15:55

for n being non zero Nat
for x, y being Point of (CarProduct ((Seg n) --> RNS_Real))
for px, py, pxy being b₁ -element FinSequence of REAL st x = PtCarProduct px & y = PtCarProduct py & x - y = PtCarProduct pxy holds
for i being Nat st i in Seg n holds
pxy . i = (px . i) - (py . i)

proof end;

theorem :: MEASUR15:56

for n being non zero Nat
for x being Point of (CarProduct ((Seg n) --> RNS_Real))
for r being Real
for px being b₁ -element FinSequence of REAL st x = PtCarProduct px holds
ex prx being b₁ -element FinSequence of REAL st r * x = PtCarProduct prx

proof end;

theorem :: MEASUR15:57

for n being non zero Nat
for x being Point of (CarProduct ((Seg n) --> RNS_Real))
for r being Real
for px, prx being b₁ -element FinSequence of REAL st x = PtCarProduct px & r * x = PtCarProduct prx holds
for i being Nat st i in Seg n holds
prx . i = r * (px . i)

proof end;

theorem Th58: :: MEASUR15:58

for n being non zero Nat
for x being Point of (CarProduct ((Seg n) --> RNS_Real))
for px being b₁ -element FinSequence of REAL st x = PtCarProduct px holds
ex nrx being Element of REAL n st
( ( for i being Nat st i in Seg n holds
nrx . i = |.(px . i).| ) & ||.x.|| = |.nrx.| )

proof end;

theorem Th59: :: MEASUR15:59

for n being non zero Nat
for x being Point of (CarProduct ((Seg n) --> RNS_Real))
for px being b₁ -element FinSequence of REAL
for r being Real st 0 <= r & x = PtCarProduct px & ( for i being Nat st i in Seg n holds
|.(px . i).| <= r / n ) holds
||.x.|| <= r

proof end;

Lm11: for n being non zero Nat
for x, y being Point of (CarProduct ((Seg n) --> RNS_Real))
for px, py being b₁ -element FinSequence of REAL
for r being Real st 0 <= r & x = PtCarProduct px & y = PtCarProduct py & ( for i being Nat st i in Seg n holds
|.((px . i) - (py . i)).| <= r / n ) holds
||.(x - y).|| <= r

proof end;

theorem Th60: :: MEASUR15:60

for n being non zero Nat
for A being set st A c= CarProduct ((Seg n) --> REAL) & A /\ (CarProduct ((Seg n) --> RAT)) <> {} holds
ex p being sequence of (CarProduct ((Seg n) --> REAL)) st rng p = A /\ (CarProduct ((Seg n) --> RAT))

proof end;

theorem Th61: :: MEASUR15:61

for n being non zero Nat
for D being non-empty b₁ -element FinSequence
for px being b₁ -element FinSequence holds
( PtCarProduct px in CarProduct D iff for i being Nat st i in Seg n holds
px . i in D . i )

proof end;

theorem Th62: :: MEASUR15:62

for n being non zero Nat
for r being Real
for f being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real st f is_continuous_on dom f holds
ex H being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( H /\ (dom f) = f " ].-infty,r.[ & H is open )

proof end;

Th63: for n being non zero Nat
for r being Real
for g being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL holds less_dom (g,r) = g " ].-infty,r.[
by MESFUN16:17;

theorem Th65: :: MEASUR15:63

for n being non zero Nat
for z being Point of (CarProduct ((Seg n) --> RNS_Real))
for r being Real st 0 < r holds
ex s being Real ex x being b₁ -element FinSequence of REAL ex D being non-empty b₁ -element FinSequence st
( 0 < s & s < r & z = PtCarProduct x & ( for i being Nat st i in Seg n holds
D . i = ].((x . i) - s),((x . i) + s).[ ) & CarProduct D c= Ball (z,r) )

proof end;

theorem Th66: :: MEASUR15:64

for n being non zero Nat
for A being Subset of (CarProduct ((Seg n) --> RNS_Real)) st A is open & ( for a being b₁ -element FinSequence of REAL st PtCarProduct a in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & ex D being non-empty b₁ -element FinSequence st
( ( for i being Nat st i in Seg n holds
D . i = ].((a . i) - r),((a . i) + r).[ ) & CarProduct D c= A ) ) } ) ) holds
ex F being Function of A,REAL st
for a being b₁ -element FinSequence of REAL st PtCarProduct a in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & ex D being non-empty b₁ -element FinSequence st
( ( for i being Nat st i in Seg n holds
D . i = ].((a . i) - r),((a . i) + r).[ ) & CarProduct D c= A ) ) } & F . (PtCarProduct a) = (upper_bound Rx) / 2 )

proof end;

theorem Th67: :: MEASUR15:65

for n being non zero Nat
for A being Subset of (CarProduct ((Seg n) --> RNS_Real)) st A is open holds
A in Prod_Field (L-Field n)

proof end;

theorem :: MEASUR15:66

for n being non zero Nat
for f being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for g being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL
for E being Element of Prod_Field (L-Field n) st f = g & f is_continuous_on E & dom f = E holds
g is E -measurable

proof end;

theorem Th69: :: MEASUR15:67

for n being non zero Nat
for px being object holds
( px is b₁ -element FinSequence of REAL iff px in product ((Seg n) --> REAL) )

proof end;

theorem :: MEASUR15:68

for n being non zero Nat
for x being object holds
( x in CarProduct ((Seg n) --> REAL) iff ex px being b₁ -element FinSequence of REAL st
( px in product ((Seg n) --> REAL) & x = PtCarProduct px ) )

proof end;

theorem Th71: :: MEASUR15:69

for n being non zero Nat holds carr ((Seg n) --> RNS_Real) = (Seg n) --> REAL

proof end;

theorem Th72: :: MEASUR15:70

for n being non zero Nat holds CarProd ((Seg n) --> RNS_Real) = CarProd ((Seg n) --> REAL)

proof end;

theorem Th73: :: MEASUR15:71

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
D . i c= REAL ) holds
product D = (CarProd ((Seg n) --> REAL)) .: (CarProduct D)

proof end;

theorem Th74: :: MEASUR15:72

for n being non zero Nat ex I being LinearOperator of (CarProduct ((Seg n) --> RNS_Real)),(product ((Seg n) --> RNS_Real)) st
( I = CarProd ((Seg n) --> RNS_Real) & I is one-to-one & I is onto & I is isometric )

proof end;

theorem :: MEASUR15:73

for n being non zero Nat
for s being sequence of (CarProduct ((Seg n) --> RNS_Real)) holds
( s is convergent iff (CarProd ((Seg n) --> RNS_Real)) * s is convergent )

proof end;

theorem Th76: :: MEASUR15:74

for n being non zero Nat
for X being Subset of (CarProduct ((Seg n) --> RNS_Real))
for Y being Subset of (product ((Seg n) --> RNS_Real)) st Y = (CarProd ((Seg n) --> RNS_Real)) .: X holds
( ( X is closed implies Y is closed ) & ( Y is closed implies X is closed ) & ( X is open implies Y is open ) & ( Y is open implies X is open ) & ( X is compact implies Y is compact ) & ( Y is compact implies X is compact ) )

proof end;

theorem :: MEASUR15:75

for n being non zero Nat
for Z being RealNormSpace
for y being Point of (product ((Seg n) --> RNS_Real))
for x being Point of (CarProduct ((Seg n) --> RNS_Real))
for f being PartFunc of (product ((Seg n) --> RNS_Real)),Z st y = (CarProd ((Seg n) --> RNS_Real)) . x & y in dom f holds
( f is_continuous_in y iff f * (CarProd ((Seg n) --> RNS_Real)) is_continuous_in x )

proof end;

theorem :: MEASUR15:76

for n being non zero Nat
for Z being RealNormSpace
for X being Subset of (product ((Seg n) --> RNS_Real))
for Y being Subset of (CarProduct ((Seg n) --> RNS_Real))
for f being PartFunc of (product ((Seg n) --> RNS_Real)),Z st Y = (CarProd ((Seg n) --> RNS_Real)) " X holds
( f is_continuous_on X iff f * (CarProd ((Seg n) --> RNS_Real)) is_continuous_on Y )

proof end;

theorem :: MEASUR15:77

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) holds
ex E being Subset of (product ((Seg n) --> RNS_Real)) st
( E = product D & E is compact )

proof end;

theorem :: MEASUR15:78

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is Element of L-Field ) holds
product D is Element of XL-Field n

proof end;

theorem :: MEASUR15:79

for n being non zero Nat
for Y being Subset of (product ((Seg n) --> RNS_Real)) st Y is open holds
Y in XL-Field n

proof end;

theorem Th82: :: MEASUR15:80

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for F being Set_Sequence of S st T is bijective holds
((.: T) | S) * F is Set_Sequence of CopyField (T,S)

proof end;

theorem Th83: :: MEASUR15:81

for X, Y being non empty set
for T being Function of X,Y
for S being SigmaField of X
for M being sigma_Measure of S st T is bijective & M is sigma_finite holds
CopyMeasure (T,M) is sigma_finite

proof end;

theorem :: MEASUR15:82

for n being non zero Nat holds XL-Meas n is sigma_finite

proof end;

theorem Th85: :: MEASUR15:83

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st rng D c= L-Field holds
CarProduct D in Prod_Field (L-Field n)

proof end;

theorem Th86: :: MEASUR15:84

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st rng D c= L-Field & ( for i being Nat st i in Seg n holds
L-Meas . (D . i) in REAL ) holds
ex E being b₁ -element FinSequence of REAL st
( ( for i being Nat st i in Seg n holds
E . i = L-Meas . (D . i) ) & (Prod_Measure (L-Meas n)) . (CarProduct D) = Product E )

proof end;

theorem :: MEASUR15:85

for n being non zero Nat
for D being non-empty b₁ -element FinSequence st rng D c= L-Field & ( for i being Nat st i in Seg n holds
L-Meas . (D . i) in REAL ) holds
ex E being b₁ -element FinSequence of REAL st
( ( for i being Nat st i in Seg n holds
E . i = L-Meas . (D . i) ) & (XL-Meas n) . (product D) = Product E )

proof end;