:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 4.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/4.0/.
environ
vocabularies MEASUR14, MEASUR13, FINSEQ_1, FINSEQ_2, NUMBERS, XXREAL_0,
SUBSET_1, CARD_1, ARYTM_3, ARYTM_1, RELAT_1, REAL_1, FUNCT_1, XBOOLE_0,
TARSKI, ZFMISC_1, PROB_1, SUPINF_2, VALUED_0, PARTFUN1, MEASURE1,
MESFUNC1, MEASUR10, MEASUR11, COMPLEX1, MESFUN12, ORDINAL2, NAT_1,
ORDINAL4, FUNCT_2, FUNCOP_1, CARD_3, SEQ_2, XCMPLX_0, MEASURE5, XXREAL_1,
MEASUR12, DUALSP02, CFCONT_1, RCOMP_1, PRE_TOPC, METRIC_1, MEMBERED,
XXREAL_2, SEQ_4, GROUP_2, PRVECT_1, PRVECT_2, ALGSTR_0, RLVECT_1,
STRUCT_0, RVSUM_1, SQUARE_1, NORMSP_1, NORMSP_0, RAT_1, FINSET_1, SEQ_1,
ORDINAL1, XREAL_0, FCONT_1, LOPBAN_1, VECTMETR, MEASURE8, MEASUR15;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, FUNCOP_1,
CARD_1, CARD_3, FINSET_1, NUMBERS, MEMBERED, XXREAL_3, XCMPLX_0,
XXREAL_0, XREAL_0, VALUED_0, RAT_1, NAT_1, XXREAL_2, SQUARE_1, COMPLEX1,
MESFUNC1, FINSEQ_1, FINSEQ_2, EUCLID, RVSUM_1, PROB_1, RCOMP_1, FINSUB_1,
MEASURE1, MEASURE5, MEASUR12, MESFUNC6, MEASURE8, MEASUR10, MEASUR11,
MESFUN12, MEASUR13, MESFUN16, MEASUR14, SEQ_1, SEQ_2, SEQ_4, STRUCT_0,
ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, NFCONT_1, LOPBAN_1,
LOPBAN_5, PRVECT_1, PRVECT_2, PRVECT_3, DUALSP02, MAZURULM;
constructors MEASUR11, MESFUN12, MESFUNC6, SQUARE_1, MEASUR12, INTEGRA1,
WSIERP_1, COMSEQ_2, PROB_3, MEASUR14, NEWTON, SEQ_2, SEQ_4, BINOP_2,
NFCONT_1, DUALSP02, LOPBAN_5, NDIFF_8, PRVECT_4, MAZURULM, MESFUN16,
SUPINF_1;
registrations ORDINAL1, XBOOLE_0, SUBSET_1, XXREAL_0, XREAL_0, NAT_1, NUMBERS,
VALUED_0, RELSET_1, MEASURE1, FINSEQ_1, FINSEQ_2, FUNCT_1, FUNCT_2,
FUNCOP_1, CARD_1, CARD_3, PRVECT_3, MEMBERED, XXREAL_2, SRINGS_4,
FINSUB_1, SETFAM_1, MEASUR13, EUCLID, SQUARE_1, TOPGEN_4, STRUCT_0,
NORMSP_0, NORMSP_1, RAT_1, FOMODEL0, PRVECT_2, PRVECT_1, FINSEQ_9,
FINSET_1, MEASURE5, COMPLEX1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
definitions TARSKI;
equalities FINSEQ_1, MEASUR10, BINOP_1, PRVECT_3, MEASUR13, RCOMP_1, ALGSTR_0,
NORMSP_0, SQUARE_1, DUALSP02, LOPBAN_5, RLVECT_1, PRVECT_2;
expansions TARSKI, XBOOLE_0, FUNCT_1, NORMSP_1, NFCONT_1;
theorems XBOOLE_0, FUNCT_1, XXREAL_0, XBOOLE_1, VALUED_0, FUNCT_2, RELAT_1,
EXTREAL1, PARTFUN1, MEASUR10, MEASUR11, MESFUN12, MESFUNC6, FINSEQ_1,
FINSEQ_2, TARSKI, ZFMISC_1, NAT_1, FUNCOP_1, XREAL_1, PROB_1, ORDINAL1,
MEASURE8, CARD_1, XTUPLE_0, CARD_3, PRVECT_3, FINSEQ_3, XREAL_0,
FINSUB_1, MEASUR13, SRINGS_5, MEASUR12, MESFUN16, COMPLEX1, MEASURE5,
PRVECT_1, PRVECT_2, RVSUM_1, EUCLID, EUCLID_3, SQUARE_1, MEASUR14,
RLVECT_1, CARD_4, RAT_1, SEQ_4, NUMBERS, RCOMP_1, SEQ_2, DUALSP03,
NORMSP_1, BINOP_2, XCMPLX_1, LOPBAN11, NFCONT_1, NDIFF_1, MEMBERED,
NDIFF_8, XXREAL_2, INTEGRA6, NDIFF_7, VECTSP_1, LOPBAN_1;
schemes RECDEF_1, FINSEQ_1, NAT_1, FUNCT_2;
begin :: Product space of real linear spaces
Lm9:
for x,a be Real holds ex r be Real st 0 < r & x in ].a-r,a+r.[
proof
let x,a be Real;
per cases;
suppose
A1: x < a; then
A2: 0 < a-x by XREAL_1:50;
take r = (a-x)+1;
thus 0 < r by A2;
x - 1 < x & x < a + r by A1,A2,XREAL_1:40,44;
hence x in ].a-r,a+r.[;
end;
suppose
A3: a <= x; then
A4: 0 <= x-a by XREAL_1:48;
take r = x - a + 1;
thus 0 < r by A4;
a-r < a by A4,XREAL_1:44; then
a-r < x & x < x + 1 by A3,XXREAL_0:2,XREAL_1:29;
hence x in ].a-r,a+r.[;
end;
end;
Lm1:
for G be RealLinearSpace-Sequence, v,w be Element of product carr G,
i be Element of dom carr G holds
([:addop G:].(v,w)).i = (the addF of G.i).(v.i,w.i)
& for vi,wi be VECTOR of G.i st vi=v.i & wi=w.i holds
([:addop G:].(v,w)).i = vi + wi
proof
let G be RealLinearSpace-Sequence, v,w be Element of product carr G,
i be Element of dom carr G;
([:addop G:].(v,w)).i = ((addop G).i).(v.i,w.i) by PRVECT_1:def 8;
hence thesis by PRVECT_1:def 12;
end;
Lm2:
for G be RealLinearSpace-Sequence, r be Element of REAL,
v be Element of product carr G, i be Element of dom carr G holds
([:multop G:].(r,v)).i = (the Mult of G.i).(r,v.i)
& for vi be VECTOR of G.i st vi=v.i holds ([:multop G:].(r,v)).i = r*vi
proof
let G be RealLinearSpace-Sequence, r be Element of REAL,
v be Element of product carr G, i be Element of dom carr G;
([:multop G:].(r,v)).i = ((multop G).i).(r,v.i) by PRVECT_2:def 2;
hence thesis by PRVECT_2:def 8;
end;
theorem
for G be RealLinearSpace-Sequence, v,w,s be Element of product G,
v1,w1,s1 be Element of product carr G st v = v1 & w = w1 & s = s1 holds
s = v + w iff
for i be Element of dom carr G, vi,wi be VECTOR of G.i
st vi = v1.i & wi = w1.i holds s1.i = vi + wi
proof
let G be RealLinearSpace-Sequence, v,w,s be Element of product G,
v1,w1,s1 be Element of product carr G;
assume
A1: v = v1 & w = w1 & s = s1;
hence s = v + w implies
for i be Element of dom carr G, vi,wi be VECTOR of G.i
st vi = v1.i & wi=w1.i holds s1.i =vi + wi by Lm1;
assume
A2: for i be Element of dom carr G, vi,wi be VECTOR of G.i st
vi = v1.i & wi = w1.i holds s1.i = vi + wi;
A3: ex g be Function st s1 = g & dom g = dom carr G &
for y being object st y in dom carr G holds g.y in (carr G).y
by CARD_3:def 5; then
dom s1 = Seg len carr G by FINSEQ_1:def 3; then
A4: dom s1 = Seg len G by PRVECT_1:def 11;
now let i be object;
assume
A5: i in dom s1; then
reconsider j=i as Element of dom G by A4,FINSEQ_1:def 3;
A6: (carr G).i = the carrier of (G.j) by PRVECT_1:def 11;
now let v be Element of product carr G;
ex g be Function st v = g & dom g = dom carr G &
for y being object st y in dom carr G holds g.y in (carr G).y
by CARD_3:def 5;
hence v.j in (carr G).j by A3,A5;
end; then
reconsider v1j = v1.j, w1j = w1.j as VECTOR of (G.j) by A6;
s1.j = v1j + w1j by A2,A3,A5;
hence s1.i = ([:addop G:].(v1,w1)).i by A3,A5,Lm1;
end; then
s1 = [:addop G:].(v1,w1) by A3,CARD_3:9;
hence s = v+w by A1;
end;
theorem
for G be RealLinearSpace-Sequence, r be Element of REAL,
v,w be Element of product G, v1,w1 be Element of product carr G st
v=v1 & w=w1 holds w = r*v iff
for i be Element of dom carr G, vi be VECTOR of G.i
st vi = v1.i holds w1.i = r*vi
proof
let G be RealLinearSpace-Sequence,
r be Element of REAL, v,w be Element of product G,
v1,w1 be Element of product carr G;
assume that
A1: v = v1 and
A2: w = w1;
thus w = r*v implies
for i be Element of dom carr G, vi be VECTOR of G.i st
vi = v1.i holds w1.i = r * vi by A1,A2,Lm2;
assume
A3: for i be Element of dom carr G, vi be VECTOR of G.i st
vi = v1.i holds w1.i = r*vi;
A4: ex g be Function st w1 = g & dom g = dom carr G &
for y being object st y in dom carr G holds g.y in (carr G).y
by CARD_3:def 5; then
dom w1 = Seg len carr G by FINSEQ_1:def 3; then
A5: dom w1 = Seg len G by PRVECT_1:def 11;
now let i be object;
assume
A6: i in dom w1; then
reconsider j=i as Element of dom G by A5,FINSEQ_1:def 3;
A7: (carr G).i = the carrier of (G.j) by PRVECT_1:def 11;
now let v be Element of product carr G;
ex g be Function st v = g & dom g = dom carr G &
for y being object st y in dom carr G holds g.y in (carr G).y
by CARD_3:def 5;
hence v.j in (carr G).j by A4,A6;
end; then
reconsider v1j = v1.j as VECTOR of (G.j) by A7;
w1.j = r * v1j by A3,A4,A6;
hence w1.i = ([:multop G:].(r,v1)).i by A4,A6,Lm2;
end; then
w1 = [:multop G:].(r,v1) by A4,CARD_3:9;
hence w = r*v by A1,A2;
end;
Lm3:
for x be Element of REAL 1, r be Real st x = <*r*> holds |.x.| = |.r.|
proof
let x be Element of REAL 1, r be Real;
assume x =<*r*>; then
sqr x = <*(r ^2)*> by RVSUM_1:55; then
Sum sqr x = r ^2 by RVSUM_1:73; then
sqrt Sum sqr x = |.r.| by COMPLEX1:72;
hence thesis by EUCLID:def 5;
end;
Lm4:
for p,q,w be FinSequence of REAL, r be Element of REAL st
w = <*|.p.|,r*> & q = p^<*r*> holds |.w.| = |.q.|
proof
let p,q,w be FinSequence of REAL, r be Element of REAL;
reconsider qq = <*r*> as FinSequence of REAL;
assume
A1: w = <*|.p.|,r *> & q = p^<*r*>; then
len w = 2 & w.1 =|.p.| & w.2 =r by FINSEQ_1:44; then
A2: |.w.| = sqrt ((|.p.|^2) + (r^2)) by EUCLID_3:22;
A3: 0 <= Sum (sqr p) by RVSUM_1:86;
|.p.|^2 = (sqrt (Sum (sqr p))) ^2 by EUCLID:def 5; then
A4: |.p.|^2 = Sum (sqr p) by A3,SQUARE_1:def 2;
sqr q = (sqr p)^(sqr qq) by A1,RVSUM_1:144; then
sqr q = (sqr p)^<*r^2*> by RVSUM_1:55; then
Sum (sqr p) + r^2 = Sum (sqr q) by RVSUM_1:74;
hence |.w.| = |.q.| by A2,A4,EUCLID:def 5;
end;
definition
let n be non zero Nat, p be n-element FinSequence;
func PtProdFinSeq p -> n-element FinSequence means :Def1:
it.1 = p.1
& for i be non zero Nat st i < n holds it.(i+1) = [it.i,p.(i+1)];
existence
proof
defpred Q[Nat,object,object] means $3 = [$2,p.($1+1)];
A1: for i being Nat st 1 <= i & i < n holds
for x being set ex y being set st Q[i,x,y]
proof
let i be Nat;
assume 1 <= i & i < n;
let x be set;
reconsider y = [x,p.(i+1)] as set by TARSKI:1;
take y;
thus thesis;
end;
consider F being FinSequence such that
A2: len F = n & (F.1 = p.1 or n = 0)
& for i be Nat st 1 <= i & i < n holds Q[i, F.i, F.(i+1)]
from RECDEF_1:sch 3(A1);
reconsider F as n-element FinSequence by A2,CARD_1:def 7;
take F;
thus thesis by A2,NAT_1:14;
end;
uniqueness
proof
let F1,F2 be n-element FinSequence;
assume that
A3: F1.1 = p.1
& for i be non zero Nat st i < n holds F1.(i+1) = [F1.i,p.(i+1)] and
A4: F2.1 = p.1
& for i be non zero Nat st i < n holds F2.(i+1) = [F2.i,p.(i+1)];
defpred P[Nat,object,object] means $3 = [$2,p.($1+1)];
A5: for i be Nat st 1 <= i & i < n
for x,y1,y2 being set st P[i,x,y1] & P[i,x,y2] holds y1 = y2;
A6: dom F1 = Seg n & dom F2 = Seg n by FINSEQ_1:89;
A7: dom F1 = Seg len F1 & dom F2 = Seg len F2 by FINSEQ_1:def 3; then
A8: len F1 = n & (F1.1 = p.1 or n = 0)
& for i be Nat st 1 <= i & i < n holds P[i,F1.i,F1.(i+1)]
by A3,A6,FINSEQ_1:6;
A9: len F2 = n & (F2.1 = p.1 or n = 0)
& for i be Nat st 1 <= i & i < n holds P[i,F2.i,F2.(i+1)]
by A4,A6,A7,FINSEQ_1:6;
thus F1 = F2 from RECDEF_1:sch 7(A5,A8,A9);
end;
end;
definition
let n be non zero Nat, p be n-element FinSequence;
func PtCarProduct p -> set equals
(PtProdFinSeq p).n;
coherence;
end;
theorem Th3:
for n,m be non zero Nat, p be n-element FinSequence,
q be m-element FinSequence
st m <= n & q = p|m holds PtProdFinSeq q = (PtProdFinSeq p) | m
proof
let n,m be non zero Nat, p be n-element FinSequence,
q be m-element FinSequence;
assume that
A1: m <= n and
A2: q = p|m;
1 <= m by NAT_1:14; then
A3: 1 in Seg m; then
A4: ((PtProdFinSeq p) |m).1 = (PtProdFinSeq p).1 by FUNCT_1:49;
defpred P[Nat,object,object] means $3 = [$2,p.($1+1)];
A5: for k be Nat st 1 <= k & k < m
for x,y1,y2 be set st P[k,x,y1] & P[k,x,y2] holds y1 = y2;
A6: for k be Nat st 1 <= k & k < m holds
P[ k,(PtProdFinSeq q).k,(PtProdFinSeq q).(k+1) ]
proof
let k be Nat;
assume that
A7: 1 <= k and
A8: k < m;
reconsider k1=k as non zero Nat by A7;
1 <= k1+1 & k1+1 <= m by A7,A8,NAT_1:13; then
k1+1 in Seg m; then
q.(k1+1) = p.(k1+1) by A2,FUNCT_1:49;
hence thesis by A8,Def1;
end;
A9: for k be Nat st 1 <= k & k < m holds
P[ k,((PtProdFinSeq p) |m).k,((PtProdFinSeq p) |m).(k+1) ]
proof
let k be Nat;
assume that
A10: 1 <= k and
A11: k < m;
reconsider k1=k as non zero Nat by A10;
A12: k1 < n by A1,A11,XXREAL_0:2;
1 <= k1+1 & k1+1 <= m by A10,A11,NAT_1:13; then
k1+1 in Seg m; then
A13: ((PtProdFinSeq p) |m).(k+1) = (PtProdFinSeq p).(k+1) by FUNCT_1:49;
k in Seg m by A10,A11; then
((PtProdFinSeq p) |m).k = (PtProdFinSeq p).k by FUNCT_1:49;
hence thesis by A13,A12,Def1;
end;
(PtProdFinSeq q).1 = q.1 by Def1; then
A14: len PtProdFinSeq q = m
& ((PtProdFinSeq q).1 = p.1 or m = 0)
& for k be Nat st 1 <= k & k < m holds
P[ k,(PtProdFinSeq q).k,(PtProdFinSeq q).(k+1) ]
by A6,A2,A3,FUNCT_1:49,CARD_1:def 7;
len (PtProdFinSeq p) = n by CARD_1:def 7; then
A15: len ((PtProdFinSeq p) |m) = m
& (((PtProdFinSeq p) |m).1 = p.1 or m = 0)
& for k be Nat st 1 <= k & k < m holds
P[ k,((PtProdFinSeq p) |m).k,((PtProdFinSeq p) |m).(k+1) ]
by A4,A9,A1,Def1,FINSEQ_1:59;
thus thesis from RECDEF_1:sch 7(A5,A14,A15);
end;
theorem Th4:
for n be non zero Nat, p be (n+1)-element FinSequence,
q be n-element FinSequence st q = p|n holds
PtCarProduct p = [PtCarProduct q,p.(n+1)]
proof
let n be non zero Nat, p be (n+1)-element FinSequence,
q be n-element FinSequence;
assume q = p|n; then
A1: PtCarProduct q = ((PtProdFinSeq p) |n).n by Th3,NAT_1:12;
n < n + 1 by NAT_1:13; then
PtCarProduct p = [ (PtProdFinSeq p).n,p.(n+1) ] by Def1;
hence thesis by A1,FINSEQ_1:3,FUNCT_1:49;
end;
theorem Th5:
for n be non zero Nat, p1,p2 be n-element FinSequence holds
PtCarProduct p1 = PtCarProduct p2 iff p1 = p2
proof
defpred P[non zero Nat] means
for p1,p2 be $1-element FinSequence holds
PtCarProduct p1 = PtCarProduct p2 iff p1 = p2;
A1: P[1]
proof
let p1,p2 be 1-element FinSequence;
hereby assume
A2: PtCarProduct p1 = PtCarProduct p2;
A3: PtCarProduct p2 = p2.1 by Def1;
A4: len p1=1 & len p2=1 by CARD_1:def 7; then
p1 = <*p1.1*> by FINSEQ_1:40;
hence p1 =p2 by A2,A3,A4,Def1,FINSEQ_1:40;
end;
thus thesis;
end;
A5: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A6: P[n];
let p1,p2 be (n+1)-element FinSequence;
hereby assume
A7: PtCarProduct p1 = PtCarProduct p2;
reconsider q1 = p1|n, q2 = p2|n as n-element FinSequence;
PtCarProduct p1 = [PtCarProduct q1,p1.(n+1)]
& PtCarProduct p2 = [PtCarProduct q2,p2.(n+1)] by Th4; then
A8: PtCarProduct q1 = PtCarProduct q2 & p1.(n+1) = p2.(n+1)
by A7,XTUPLE_0:1;
A9: len p1 = n+1 & len p2 = n+1 by CARD_1:def 7; then
p1 = q1^<*p1.(n+1)*> by FINSEQ_3:55;
hence p1 = p2 by A6,A8,A9,FINSEQ_3:55;
end;
thus thesis;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A5);
hence thesis;
end;
theorem Th6:
for n be non zero Nat, X be non-empty n-element FinSequence, x be object
holds x in CarProduct X iff
ex px be n-element FinSequence st px in product X & x = PtCarProduct px
proof
defpred P[non zero Nat] means
for X be non-empty $1-element FinSequence, x be object
holds x in CarProduct X iff
ex px be $1-element FinSequence st px in product X & x = PtCarProduct px;
A1: P[1]
proof
let X be non-empty 1-element FinSequence;
set P = ProdFinSeq X;
A2: CarProduct X = X.1 by MEASUR13:def 3;
let x be object;
hereby assume
A3: x in CarProduct X;
reconsider px = <*x*> as 1-element FinSequence;
take px;
dom px = Seg len px & dom X = Seg len X by FINSEQ_1:def 3; then
A4: dom px = Seg 1 & dom X = Seg 1 by CARD_1:def 7;
now let s be object;
assume
A5: s in dom X; then
reconsider i = s as Nat;
i = 1 by A4,A5,FINSEQ_1:2,TARSKI:def 1;
hence px.s in X.s by A3,MEASUR13:def 3;
end;
hence px in product X by A4,CARD_3:def 5;
(PtProdFinSeq px).1 = px.1
& for i be non zero Nat st i < 1 holds
(PtProdFinSeq px).(i+1) = [(PtProdFinSeq px).i, px.(i+1)] by Def1;
hence x = PtCarProduct px;
end;
given px be 1-element FinSequence such that
A6: px in product X & x = PtCarProduct px;
A7: ex g be Function st px = g & dom g = dom X
& for y being object st y in dom X holds g.y in X.y by A6,CARD_3:def 5;
A8: PtCarProduct px = px.1 by Def1;
1 in Seg 1; then
1 in Seg len X by CARD_1:def 7; then
1 in dom X by FINSEQ_1:def 3;
hence x in CarProduct X by A2,A6,A8,A7;
end;
A9:for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A10: P[n];
let X be non-empty (n+1)-element FinSequence;
set Xn1 = ElmFin(X,n+1);
A11: Xn1 = X.(n+1) by MEASUR13:def 1;
set Xn = SubFin(X,n);
A12: Xn = X|n by NAT_1:11,MEASUR13:def 5;
A13: CarProduct X = [: CarProduct SubFin(X,n),ElmFin(X,n+1) :]
by MEASUR13:6;
let x be object;
thus x in CarProduct X iff
ex px be (n+1)-element FinSequence
st px in product X & x = PtCarProduct px
proof
hereby assume x in CarProduct X; then
consider y,z be object such that
A14: y in CarProduct Xn & z in X.(n+1) & x = [y,z]
by A11,A13,ZFMISC_1:def 2;
consider py be n-element FinSequence such that
A15: py in product Xn & y = PtCarProduct py by A14,A10;
A16: ex g be Function st py = g & dom g = dom Xn &
for y being object st y in dom Xn holds g.y in Xn.y
by CARD_3:def 5,A15;
reconsider px = py^<*z*> as (n+1)-element FinSequence;
A17: len py = n by CARD_1:def 7; then
A18: px.(n+1) = z by FINSEQ_1:42;
dom px = Seg len px by FINSEQ_1:def 3; then
A19: dom px = Seg (n+1) by CARD_1:def 7;
dom X = Seg len X by FINSEQ_1:def 3; then
A20: dom X = Seg (n+1) by CARD_1:def 7;
take px;
for s be object st s in dom X holds px.s in X.s
proof
let s be object;
assume
A21: s in dom X; then
reconsider i = s as Nat;
A22: 1 <= i & i <= n+1 by A20,A21,FINSEQ_1:1;
per cases;
suppose i <> n+1; then
i < n+1 by A22,XXREAL_0:1; then
i <= n by NAT_1:13; then
A23: i in Seg n by A22; then
i in Seg len Xn by CARD_1:def 7; then
i in dom Xn by FINSEQ_1:def 3; then
A24: py.i in Xn.i by A16;
A25: X.i = Xn.i by A12,A23,FUNCT_1:49;
i in dom py by A23,A17,FINSEQ_1:def 3;
hence px.s in X.s by A25,A24,FINSEQ_1:def 7;
end;
suppose i = n+1;
hence px.s in X.s by A14,A17,FINSEQ_1:42;
end;
end;
hence px in product X by A19,A20,CARD_3:def 5;
reconsider px1 = px|n as n-element FinSequence;
dom py = Seg n by A17,FINSEQ_1:def 3; then
py = px|n by FINSEQ_1:21;
hence x = PtCarProduct px by A18,A14,A15,Th4;
end;
assume ex px be (n+1)-element FinSequence
st px in product X & x = PtCarProduct px; then
consider px be (n+1)-element FinSequence such that
A26: px in product X & x = PtCarProduct px;
A27: ex g be Function st px = g & dom g = dom X &
for y being object st y in dom X holds g.y in X.y by A26,CARD_3:def 5;
reconsider py = px|n as n-element FinSequence;
A28: PtCarProduct px = [ PtCarProduct py,px.(n+1) ] by Th4;
dom py = Seg len py by FINSEQ_1:def 3; then
A29: dom py = Seg n by CARD_1:def 7;
dom Xn = Seg len Xn by FINSEQ_1:def 3; then
A30: dom Xn = Seg n by CARD_1:def 7;
set y = PtCarProduct py;
for s be object st s in dom Xn holds py.s in Xn.s
proof
let s be object;
assume
A31: s in dom Xn; then
reconsider i=s as Nat;
A32: Xn.i = X.i & py.i = px.i by A12,A31,A30,FUNCT_1:49;
Seg n c= Seg (n+1) by FINSEQ_3:18; then
i in Seg (n+1) by A31,A30; then
i in Seg len X by CARD_1:def 7; then
i in dom X by FINSEQ_1:def 3;
hence py.s in Xn.s by A27,A32;
end; then
py in product Xn by A29,A30,CARD_3:def 5; then
A33: y in CarProduct Xn by A10;
n+1 in Seg (n+1) by FINSEQ_1:4; then
(n+1) in Seg len X by CARD_1:def 7; then
(n+1) in dom X by FINSEQ_1:def 3; then
px.(n+1) in Xn1 by A11,A27;
hence x in CarProduct X by A28,A33,A13,A26,ZFMISC_1:87;
end;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A9);
hence thesis;
end;
registration
let n be non empty Nat;
cluster n-element for RealNormSpace-Sequence;
correctness
proof
set X = the RealNormSpace;
set F = Seg n --> X;
A1: n is Element of NAT by ORDINAL1:def 12;
dom F = Seg n; then
A2: len F = n by A1,FINSEQ_1:def 3;
for y being set st y in rng F holds y is RealNormSpace
proof
let y be set;
assume y in rng F; then
ex x be object st x in dom F & y = F.x by FUNCT_1:def 3;
hence thesis by FUNCOP_1:7;
end; then
reconsider F as RealNormSpace-Sequence by PRVECT_2:def 10;
take F;
thus thesis by A2,CARD_1:def 7;
end;
end;
definition
let m,n be non zero Nat, X be n-element RealNormSpace-Sequence;
assume A1:m <= n;
func ElmFin(X,m) -> RealNormSpace equals :Def3:
X.m;
coherence
proof
1 <= m by NAT_1:14; then
A2: m in Seg n by A1;
len X = n by CARD_1:def 7; then
A3: m in dom X by A2,FINSEQ_1:def 3;
X.m in rng X by A3,FUNCT_1:3;
hence thesis by PRVECT_2:def 10;
end;
end;
definition
let n be non zero Nat, X be n-element RealNormSpace-Sequence;
func ProdFinSeq X -> n-element RealNormSpace-Sequence means :Def4:
it.1 = X.1
& for i be non zero Nat st i < n ex X1,X2 be RealNormSpace st
X1 = it.i & X2 = X.(i+1) & it.(i+1) = [: X1,X2 :];
existence
proof
A1: len X = n by CARD_1:def 7;
1 <= n by NAT_1:14; then
1 in Seg n; then
A2: 1 in dom X by A1,FINSEQ_1:def 3;
defpred Q[Nat,set,set] means
( ex Pi,Xi1 be RealNormSpace st Pi = $2 & Xi1 = X.($1+1) ) implies
ex Pi,Xi1,Pi1 be RealNormSpace st
Pi=$2 & Xi1 = X.($1+1) & Pi1=$3 & Pi1 = [:Pi,Xi1:];
A3: for i being Nat st 1 <= i & i < n holds
for x being set ex y being set st Q[i,x,y]
proof
let i be Nat;
assume 1 <= i & i < n;
let x be set;
now assume ex Pi,Xi1 be RealNormSpace st Pi=x & Xi1 = X.(i+1); then
consider Pi,Xi1 be RealNormSpace such that
A4: Pi = x & Xi1 = X.(i+1);
reconsider y = [:Pi,Xi1:] as RealNormSpace;
take y;
ex Pi,Xi1,Pi1 be RealNormSpace st Pi = x & Xi1 = X.(i+1)
& Pi1 = y & Pi1 = [:Pi,Xi1:] by A4;
hence thesis;
end;
hence thesis;
end;
consider P being FinSequence such that
A5: len P = n & (P.1 = X.1 or n = 0)
& for i be Nat st 1 <= i & i < n holds Q[ i,P.i,P.(i+1) ]
from RECDEF_1:sch 3(A3);
reconsider P as n-element FinSequence by A5,CARD_1:def 7;
defpred L[Nat] means
1 <= $1 & $1 < n implies
ex Pi,Xi1,Pi1 be RealNormSpace
st Pi = P.$1 & Xi1 = X.($1+1) & P.($1+1) = Pi1 & Pi1 = [:Pi,Xi1:];
A6: L[0];
A7: for i be Nat st L[i] holds L[i+1]
proof
let i be Nat;
assume
A8: L[i];
assume
A9: 1<=i+1 & i+1 < n; then
A10: (i+1)+1 <= n by NAT_1:13;
A11: i + 0 < i+1 by XREAL_1:8;
1 <= (i+1)+1 by NAT_1:12; then
(i+1)+1 in Seg n by A10; then
(i+1)+1 in dom X by A1,FINSEQ_1:def 3; then
X.((i+1)+1) in rng X by FUNCT_1:3; then
reconsider Xi1 = X.((i+1)+1) as RealNormSpace by PRVECT_2:def 10;
per cases;
suppose
A12: i = 0;
X.1 in rng X by A2,FUNCT_1:def 3; then
reconsider Pi = P.1 as RealNormSpace by A5,PRVECT_2:def 10;
Pi = P.(i+1) & Xi1 = X.((i+1)+1) by A12;
hence ex Pi,Xi1,Pi1 be RealNormSpace st Pi = P.(i+1) & Xi1 = X.((i+1)+1)
& Pi1 = P.((i+1)+1) & Pi1 = [:Pi,Xi1:] by A5,A9;
end;
suppose i <> 0; then
consider Pi0,Xi10,Pi be RealNormSpace such that
A13: Pi0 = P.i & Xi10 = X.(i+1) & P.(i+1) = Pi & Pi = [:Pi0,Xi10:]
by A8,A9,A11,XXREAL_0:2,NAT_1:14;
Pi = P.(i+1) & Xi1 = X.((i+1)+1) by A13;
hence ex Pi,Xi1,Pi1 be RealNormSpace st Pi = P.(i+1) & Xi1 = X.((i+1)+1)
& Pi1 = P.((i+1)+1) & Pi1 = [:Pi,Xi1:] by A5,A9;
end;
end;
A14:for i be Nat holds L[i] from NAT_1:sch 2(A6,A7);
defpred H[Nat] means 1 <= $1 & $1 <= n implies P.$1 is RealNormSpace;
A15:H[0];
A16:for i be Nat st H[i] holds H[i+1]
proof
let i be Nat;
assume H[i];
assume
A17: 1 <= i+1 & i+1 <= n;
A18: i+0 < i+1 by XREAL_1:8;
per cases;
suppose
A19: i = 0;
X.1 in rng X by A2,FUNCT_1:def 3;
hence P.(i+1) is RealNormSpace by A19,A5,PRVECT_2:def 10;
end;
suppose i <> 0; then
1 <= i & i < n by A17,A18,XXREAL_0:2,NAT_1:14; then
ex Pi,Xi1,Pi1 be RealNormSpace st Pi = P.i & Xi1 = X.(i+1)
& P.(i+1) = Pi1 & Pi1= [:Pi,Xi1:] by A14;
hence P.(i+1) is RealNormSpace;
end;
end;
A20:for i be Nat holds H[i] from NAT_1:sch 2(A15,A16);
now let y be set;
assume y in rng P; then
consider i be object such that
A21: i in dom P & y=P.i by FUNCT_1:def 3;
reconsider i as Nat by A21;
i in Seg len P by A21,FINSEQ_1:def 3; then
1 <= i & i <= n by A5,FINSEQ_1:1;
hence y is RealNormSpace by A20,A21;
end; then
reconsider P as n-element RealNormSpace-Sequence by PRVECT_2:def 10;
n in Seg n by FINSEQ_1:3; then
n in dom P by A5,FINSEQ_1:def 3; then
P.n in rng P by FUNCT_1:3; then
reconsider y = P.n as RealNormSpace by PRVECT_2:def 10;
take P;
thus P.1 = X.1 by A5;
hereby let i be non zero Nat;
assume
A22: i < n;
0+1 <= i by NAT_1:13; then
consider Pi,Xi1,Pi1 be RealNormSpace such that
A23: Pi = P.i & Xi1 = X.(i+1) & P.(i+1) = Pi1 & Pi1 = [:Pi,Xi1:] by A14,A22;
take Pi,Xi1;
thus Pi = P.i & Xi1 = X.(i+1) & P.(i+1) = [:Pi,Xi1:] by A23;
end;
end;
uniqueness
proof
let P1,P2 be n-element RealNormSpace-Sequence;
assume that
A24:P1.1 = X.1
& ( for i be non zero Nat st i < n ex X1,X2 be RealNormSpace st
X1 = P1.i & X2 = X.(i+1) & P1.(i+1) = [:X1,X2:] )
and
A25:P2.1 = X.1
& ( for i be non zero Nat st i < n ex X1,X2 be RealNormSpace st
X1 = P2.i & X2 = X.(i+1) & P2.(i+1) = [:X1,X2:] );
defpred P[Nat,set,set] means
ex Pi,Xi1 be RealNormSpace st Pi=$2 & Xi1 = X.($1+1) & $3 = [:Pi,Xi1:];
A26:for i be Nat st 1 <= i & i < n
for x,y1,y2 being set st P[i,x,y1] & P[i,x,y2] holds y1 = y2;
A27:len P1 = n & (P1.1 = X.1 or n = 0)
& for i be Nat st 1 <= i & i < n holds P[i,P1.i,P1.(i+1)]
by A24,CARD_1:def 7;
A28:len P2 = n & (P2.1 = X.1 or n = 0)
& for i be Nat st 1 <= i & i < n holds P[i,P2.i,P2.(i+1)]
by A25,CARD_1:def 7;
P1 = P2 from RECDEF_1:sch 7(A26,A27,A28);
hence thesis;
end;
end;
definition
let n be non zero Nat, X be n-element RealNormSpace-Sequence;
func CarProduct X -> RealNormSpace equals
(ProdFinSeq X).n;
coherence
proof
1 <= n by NAT_1:14; then
n in Seg n; then
n in dom ProdFinSeq X by FINSEQ_1:89; then
(ProdFinSeq X).n in rng(ProdFinSeq X) by FUNCT_1:3;
hence thesis by PRVECT_2:def 10;
end;
end;
registration
let n be non zero Nat, X be n-element RealNormSpace-Sequence;
cluster CarProduct X -> non empty;
coherence;
end;
theorem Th7:
for m,n be non zero Nat, X be n-element RealNormSpace-Sequence
st m <= n holds X|m is m-element RealNormSpace-Sequence
proof
let m,n be non zero Nat, X be n-element RealNormSpace-Sequence;
assume
A1: m <= n;
A2: len X = n by CARD_1:def 7;
set X1 = X|m;
A3: len X1 = m by A2,FINSEQ_1:59,A1; then
reconsider X1 as m-element FinSequence by CARD_1:def 7;
for y be set st y in rng X1 holds y is RealNormSpace
proof
let y be set;
assume y in rng X1; then
consider i be object such that
A4: i in dom X1 & y=X1.i by FUNCT_1:def 3;
reconsider i as Nat by A4;
A5: i in Seg len X1 by A4,FINSEQ_1:def 3;
Seg m c= Seg n by A1,FINSEQ_1:5; then
i in Seg n by A5,A3; then
i in Seg len X by CARD_1:def 7; then
i in dom X by FINSEQ_1:def 3; then
X.i in rng X by FUNCT_1:3; then
X.i is RealNormSpace by PRVECT_2:def 10;
hence y is RealNormSpace by A4,A5,A3,FUNCT_1:49;
end;
hence X|m is m-element RealNormSpace-Sequence by PRVECT_2:def 10;
end;
definition
let m,n be non zero Nat, X be n-element RealNormSpace-Sequence;
assume A1: m <= n;
func SubFin(X,m) -> m-element RealNormSpace-Sequence equals :Def6:
X|m;
correctness by A1,Th7;
end;
theorem Th8:
for i,j,k,n be non zero Nat, X be n-element RealNormSpace-Sequence
st i <= j & j <= k & k <= n holds
(ProdFinSeq SubFin(X,j)).i = (ProdFinSeq SubFin(X,k)).i
proof
let i,j,k,n be non zero Nat, X be n-element RealNormSpace-Sequence;
assume that
A1: i <= j and
A2: j <= k and
A3: k <= n;
1 <= j & 1 <= k by NAT_1:14; then
A4: 1 in Seg j & 1 in Seg k;
defpred P[Nat] means
1 <= $1 & $1 <= j implies
(ProdFinSeq SubFin(X,j)).$1 = (ProdFinSeq SubFin(X,k)).$1;
A5: P[0];
A6: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume
A7: P[m];
assume
A8: 1 <= m+1 & m+1 <= j; then
A9: m < j by NAT_1:13;
A10: m+1 <= k by A8,A2,XXREAL_0:2; then
A11: m+1 in Seg j & m+1 in Seg k by A8;
SubFin(X,j) = X|j & SubFin(X,k) = X|k by A2,A3,Def6,XXREAL_0:2; then
A12: SubFin(X,j).(m+1) = X.(m+1) & SubFin(X,k).(m+1) = X.(m+1)
by A11,FUNCT_1:49;
per cases;
suppose m = 0; then
(ProdFinSeq SubFin(X,j)).(m+1) = SubFin(X,j).1
& (ProdFinSeq SubFin(X,k)).(m+1) = SubFin(X,k).1 by Def4; then
(ProdFinSeq SubFin(X,j)).(m+1) = (X|j).1
& (ProdFinSeq SubFin(X,k)).(m+1) = (X|k).1 by A2,A3,Def6,XXREAL_0:2; then
(ProdFinSeq SubFin(X,j)).(m+1) = X.1
& (ProdFinSeq SubFin(X,k)).(m+1) = X.1 by A4,FUNCT_1:49;
hence (ProdFinSeq SubFin(X,j)).(m+1) = (ProdFinSeq SubFin(X,k)).(m+1);
end;
suppose A13: m <> 0; then
reconsider m1 = m as non zero Nat;
reconsider j1 = j-1 as non zero Nat by A13,A8,NAT_1:13,14,20;
1 <= m by A13,NAT_1:14; then
1 < j by A9,XXREAL_0:2; then
1 < k by A2,XXREAL_0:2; then
reconsider k1 = k-1 as non zero Nat by NAT_1:20;
m1 < k1+1 by A10,NAT_1:13; then
A14: ex X1,X2 be RealNormSpace st
X1 = (ProdFinSeq SubFin(X,k1+1)).m1 & X2 = SubFin(X,k1+1).(m1+1)
& (ProdFinSeq SubFin(X,k1+1)).(m1+1) = [: X1,X2 :] by Def4;
ex Y1,Y2 be RealNormSpace st
Y1 = (ProdFinSeq SubFin(X,j1+1)).m1 & Y2 = SubFin(X,j1+1).(m1+1)
& (ProdFinSeq SubFin(X,j1+1)).(m1+1) = [: Y1,Y2 :] by A9,Def4;
hence (ProdFinSeq SubFin(X,j)).(m+1) = (ProdFinSeq SubFin(X,k)).(m+1)
by A7,A8,A12,A14,NAT_1:13,14;
end;
end;
A15:for m be Nat holds P[m] from NAT_1:sch 2(A5,A6);
1 <= i by NAT_1:14;
hence (ProdFinSeq SubFin(X,j)).i = (ProdFinSeq SubFin(X,k)).i by A1,A15;
end;
theorem Th9:
for m,n be non zero Nat, X be n-element RealNormSpace-Sequence
st m <= n holds
(ProdFinSeq X).m = (ProdFinSeq SubFin(X,m)).m
proof
let m,n be non zero Nat, X be n-element RealNormSpace-Sequence;
assume
A1: m <= n;
len X = n by FINSEQ_3:153; then
X = X|n by FINSEQ_1:58; then
X = SubFin(X,n) by Def6;
hence (ProdFinSeq X).m = (ProdFinSeq SubFin(X,m)).m by A1,Th8;
end;
theorem Th10:
for n be non zero Nat, X be (n+1)-element RealNormSpace-Sequence holds
CarProduct X = [: CarProduct SubFin(X,n),ElmFin(X,n+1) :]
proof
let n be non zero Nat, X be (n+1)-element RealNormSpace-Sequence;
A1: n < n+1 by NAT_1:13; then
consider X1,X2 be RealNormSpace such that
A2: X1 = (ProdFinSeq X).n & X2 = X.(n+1) & (ProdFinSeq X).(n+1) = [:X1,X2:]
by Def4;
X1 = CarProduct SubFin(X,n) by A2,A1,Th9;
hence thesis by A2,Def3;
end;
theorem Th11:
for k,m,n be non zero Nat, X be n-element RealNormSpace-Sequence
st k <= m & m <= n holds SubFin(X,k) = SubFin(SubFin(X,m),k)
proof
let k,m,n be non zero Nat, X be n-element RealNormSpace-Sequence;
assume that
A1: k <= m and
A2: m <= n;
SubFin(X,m) = X|m by A2,Def6; then
A3: SubFin(SubFin(X,m),k) = (X|m) |k by A1,Def6;
SubFin(X,k) = X|k by A2,A1,XXREAL_0:2,Def6;
hence SubFin(X,k) = SubFin(SubFin(X,m),k) by A1,A3,FINSEQ_1:82;
end;
Lm5:
for n be non zero Nat, X be n-element RealNormSpace-Sequence holds
ex CX be non-empty n-element FinSequence st
CarProduct CX = the carrier of CarProduct X
& for i be non zero Nat st i <= n holds CX.i = the carrier of ElmFin(X,i)
proof
defpred P[non zero Nat] means
for X be $1-element RealNormSpace-Sequence holds
ex CX be non-empty $1-element FinSequence
st CarProduct CX = the carrier of CarProduct X
& for i be non zero Nat st i <= $1 holds
CX.i = the carrier of ElmFin(X,i);
A1: P[1]
proof
let X be 1-element RealNormSpace-Sequence;
len X = 1 by CARD_1:def 7; then
1 in dom X by FINSEQ_3:25; then
X.1 in rng X by FUNCT_1:3; then
reconsider X1 = X.1 as RealNormSpace by PRVECT_2:def 10;
reconsider CX = <*the carrier of X1*> as 1-element FinSequence;
rng CX = {the carrier of X1} by FINSEQ_1:38; then
not {} in rng CX; then
reconsider CX as non-empty 1-element FinSequence by RELAT_1:def 9;
take CX;
CarProduct CX = CX.1 by MEASUR13:def 3;
hence CarProduct CX = the carrier of CarProduct X by Def4;
now let i be non zero Nat;
assume
A2: i <= 0+1;
1 <= i by NAT_1:14; then
i = 1 by A2,XXREAL_0:1;
hence CX.i = the carrier of ElmFin(X,i) by Def3;
end;
hence thesis;
end;
A3: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A4: P[n];
let X be (n+1)-element RealNormSpace-Sequence;
set Xn1 = SubFin(X,n);
set Xn11 = ElmFin(X,n+1);
A5: CarProduct X = [: CarProduct SubFin(X,n),ElmFin(X,n+1) :] by Th10;
consider CXn1 be non-empty n-element FinSequence such that
A6: CarProduct CXn1 = the carrier of CarProduct Xn1
& for i be non zero Nat st i <= n holds
CXn1.i = the carrier of ElmFin(Xn1,i) by A4;
reconsider CX = CXn1^<*the carrier of Xn11*>
as (n+1)-element FinSequence;
A7: len CXn1 = n by CARD_1:def 7;
not {} in rng CX
proof
assume {} in rng CX; then
consider i be object such that
A8: i in dom CX & {} =CX.i by FUNCT_1:def 3;
reconsider i as Nat by A8;
len CX = len CXn1 + len <*the carrier of Xn11*> by FINSEQ_1:22; then
len CX = len CXn1 + 1 by FINSEQ_1:40; then
dom CX = Seg (n+1) by A7,FINSEQ_1:def 3; then
A9: 1 <= i & i <= n+1 by A8,FINSEQ_1:1;
per cases;
suppose i <> n+1; then
i < n+1 by A9,XXREAL_0:1; then
i <= n by NAT_1:13; then
i in Seg n by A9; then
A10: i in dom CXn1 by A7,FINSEQ_1:def 3; then
CX.i = CXn1.i by FINSEQ_1:def 7;
hence contradiction by A8,A10;
end;
suppose i = n+1;
hence contradiction by A8,A7,FINSEQ_1:42;
end;
end; then
reconsider CX as non-empty (n+1)-element FinSequence by RELAT_1:def 9;
take CX;
A11: CX.(n+1) = the carrier of Xn11 by A7,FINSEQ_1:42;
A12: ElmFin(CX,n+1) = CX.(n+1) by MEASUR13:def 1;
A13: dom CXn1 = Seg n by A7,FINSEQ_1:def 3; then
A14: CX|n = CXn1 by FINSEQ_1:21;
SubFin(CX,n) = CX|n by NAT_1:11,MEASUR13:def 5;
hence CarProduct CX = the carrier of CarProduct X
by A5,A6,A11,A12,A14,MEASUR13:6;
now let i be non zero Nat;
assume
A15: i <= n+1;
per cases;
suppose i <> n+1; then
i < n+1 by A15,XXREAL_0:1; then
A16: i <= n by NAT_1:13; then
A17: CXn1.i = the carrier of ElmFin(Xn1,i) by A6;
1 <= i by NAT_1:14; then
A18: i in Seg n by A16;
Xn1 = X|n by Def6,NAT_1:11; then
X.i = Xn1.i by A18,FUNCT_1:49; then
ElmFin(X,i) = Xn1.i by A15,Def3; then
ElmFin(X,i) = ElmFin(Xn1,i) by A16,Def3;
hence CX.i = the carrier of ElmFin(X,i) by A13,A18,A17,FINSEQ_1:def 7;
end;
suppose i = n+1;
hence CX.i = the carrier of ElmFin(X,i) by A7,FINSEQ_1:42;
end;
end;
hence thesis;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A3);
hence thesis;
end;
theorem Th12:
for n be non zero Nat, X be n-element RealNormSpace-Sequence holds
ex CX be non-empty n-element FinSequence st
CarProduct CX = the carrier of CarProduct X & CX = carr X
& for i be non zero Nat st i <= n holds CX.i = the carrier of ElmFin(X,i)
proof
let n be non zero Nat, X be n-element RealNormSpace-Sequence;
consider CX be non-empty n-element FinSequence such that
A1: CarProduct CX = the carrier of CarProduct X
& for i be non zero Nat st i <= n holds
CX.i = the carrier of ElmFin(X,i) by Lm5;
take CX;
A2: len CX = n by FINSEQ_3:153;
A3: len X = n by FINSEQ_3:153; then
A4: len carr X = n by PRVECT_1:def 11;
for k be Nat st k in dom CX holds CX.k = (carr X).k
proof
let k be Nat;
assume k in dom CX; then
A5: k in Seg n by A2,FINSEQ_1:def 3; then
A6: 1 <= k & k <= n by FINSEQ_1:1;
reconsider k0=k as non zero Nat by A5,FINSEQ_1:1;
reconsider k1=k as Element of dom X by A3,A5,FINSEQ_1:def 3;
A7: CX.k = the carrier of ElmFin(X,k0) by A1,A6;
ElmFin(X,k0) = X.k1 by A6,Def3;
hence CX.k = (carr X).k by A7,PRVECT_1:def 11;
end;
hence thesis by A1,A4,A2,FINSEQ_3:29;
end;
theorem Th13:
for k,m,n be non zero Nat, X be n-element RealNormSpace-Sequence
st k <= m & m <= n holds ElmFin(X,k) = ElmFin(SubFin(X,m),k)
proof
let k,m,n be non zero Nat, X be n-element RealNormSpace-Sequence;
assume that
A1: k <= m and
A2: m <= n;
A3: ElmFin(X,k) = X.k by A1,A2,Def3,XXREAL_0:2;
1 <= k by NAT_1:14; then
A4: k in Seg m by A1;
SubFin(X,m) = X|m by A2,Def6; then
ElmFin(SubFin(X,m),k) = (X|m).k by A1,Def3;
hence ElmFin(X,k) = ElmFin(SubFin(X,m),k) by A3,A4,FUNCT_1:49;
end;
theorem
for m,n be non zero Nat, X be n-element RealNormSpace-Sequence
st m < n holds
CarProduct SubFin(X,m+1) = [: CarProduct SubFin(X,m),ElmFin(X,m+1) :]
proof
let m,n be non zero Nat, X be n-element RealNormSpace-Sequence;
assume m < n; then
A1: m <= m+1 & m+1 <= n by NAT_1:13; then
A2: ElmFin(SubFin(X,m+1),m+1) = ElmFin(X,m+1) by Th13;
CarProduct SubFin(X,m+1)
= [: CarProduct SubFin(SubFin(X,m+1),m),ElmFin(SubFin(X,m+1),m+1) :]
by Th10;
hence CarProduct SubFin(X,m+1)
= [: CarProduct SubFin(X,m),ElmFin(X,m+1) :] by A1,A2,Th11;
end;
theorem
for m,n be non zero Nat, X be (n+1)-element RealNormSpace-Sequence
st m <= n holds
CarProduct SubFin(X,m) = CarProduct SubFin(SubFin(X,n),m)
proof
let m,n be non zero Nat, X be (n+1)-element RealNormSpace-Sequence;
assume A1: m <= n;
n <= n+1 by NAT_1:13;
hence thesis by A1,Th11;
end;
theorem Th16:
for n be non zero Nat, X be n-element RealNormSpace-Sequence, x be object
holds
x is Point of CarProduct X iff
ex px be n-element FinSequence st x = PtCarProduct px
& for i be non zero Nat st i <= n holds
ex pxi be Point of ElmFin(X,i) st pxi = px.i
proof
defpred P[non zero Nat] means
for X be $1-element RealNormSpace-Sequence, x be object holds
x is Point of CarProduct X
iff ex px be $1-element FinSequence st x = PtCarProduct px
& for i be non zero Nat st i <= $1 holds
ex pxi be Point of ElmFin(X,i) st pxi = px.i;
A1: P[1]
proof
let X be 1-element RealNormSpace-Sequence, x be object;
A2: ElmFin(X,1) = X.1 by Def3;
hereby assume x is Point of CarProduct X; then
reconsider x1=x as Point of ElmFin(X,1) by A2,Def4;
reconsider px = <*x1*> as 1-element FinSequence;
take px;
PtCarProduct px = px.1 by Def1;
hence x = PtCarProduct px;
now let i be non zero Nat;
assume
A3: i <= 1;
1 <= i by NAT_1:14; then
i = 1 by A3,XXREAL_0:1;
hence ex pxi be Point of ElmFin(X,i) st pxi = px.i;
end;
hence for i be non zero Nat st i <= 1
ex pxi be Point of ElmFin(X,i) st pxi=px.i;
end;
assume ex px be 1-element FinSequence st
x = PtCarProduct px
& ( for i be non zero Nat st i <= 1
ex pxi be Point of ElmFin(X,i) st pxi=px.i ); then
consider px be 1-element FinSequence such that
A4: ( for i be non zero Nat st i <= 1
ex pxi be Point of ElmFin(X,i) st pxi = px.i )
& x = PtCarProduct px;
A5: PtCarProduct px = px.1 by Def1;
ex pxi be Point of ElmFin(X,1) st pxi=px.1 by A4;
hence x is Point of CarProduct X by A4,A5,A2,Def4;
end;
A6: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A7: P[n];
let X be (n+1)-element RealNormSpace-Sequence, x be object;
set Xn = SubFin(X,n);
set Xn1 = ElmFin(X,n+1);
A8: n <= n+1 by NAT_1:11;
A9: Xn = X|n & Xn1 = X.(n+1) by Def6,Def3,NAT_1:11;
A10: CarProduct X = [: CarProduct Xn,Xn1 :] by Th10;
hereby assume
x is Point of CarProduct X; then
consider y be Point of CarProduct Xn, z be Point of Xn1 such that
A12: x = [y,z] by A10,PRVECT_3:18;
consider py be n-element FinSequence such that
A13: y = PtCarProduct py
& ( for i be non zero Nat st i <= n holds
ex pyi be Point of ElmFin(Xn,i) st pyi=py.i ) by A7;
reconsider px = py ^ <*z*> as (n+1)-element FinSequence;
A14: len py = n by CARD_1:def 7; then
A15: px.(n+1) = z by FINSEQ_1:42;
A16: for i be non zero Nat st i <= n+1 holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i
proof
let i be non zero Nat;
assume
A17: i <= n+1;
A18: 1 <= i by NAT_1:14;
per cases;
suppose i <> n+1; then
i < n+1 by A17,XXREAL_0:1; then
A19: i <= n by NAT_1:13; then
i in dom py by A14,A18,FINSEQ_3:25; then
A20: px.i = py.i by FINSEQ_1:def 7;
ElmFin(X,i) = ElmFin(Xn,i) by A8,A19,Th13;
hence ex pxi be Point of ElmFin(X,i) st pxi=px.i by A13,A19,A20;
end;
suppose i = n+1;
hence ex pxi be Point of ElmFin(X,i) st pxi=px.i by A15;
end;
end;
dom py = Seg n by A14,FINSEQ_1:def 3; then
A21: py = px|n by FINSEQ_1:21;
reconsider px1 = px|n as n-element FinSequence;
PtCarProduct px = [PtCarProduct px1,px.(n+1)] by Th4;
hence ex px be (n+1)-element FinSequence st
x= PtCarProduct px
& ( for i be non zero Nat st i <= n+1 holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i ) by A16,A15,A21,A12,A13;
end;
assume ex px be (n+1)-element FinSequence st
x = PtCarProduct px
& ( for i be non zero Nat st i <= n+1 holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i ); then
consider px be (n+1)-element FinSequence such that
A22: ( for i be non zero Nat st i <= n+1 holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i )
& x = PtCarProduct px;
A23: n <= n+1 by NAT_1:11;
reconsider py = px|n as n-element FinSequence;
for i be non zero Nat st i <= n holds
ex pyi be Point of ElmFin(Xn,i) st pyi=py.i
proof
let i be non zero Nat;
assume
A24: i <= n;
1 <= i by NAT_1:14; then
i in Seg n by A24; then
A25: Xn.i = X.i & py.i = px.i by A9,FUNCT_1:49;
ElmFin(Xn,i) = ElmFin(X,i) by A23,A24,Th13;
hence thesis by A22,A25,A23,A24,XXREAL_0:2;
end; then
reconsider y = PtCarProduct py as Point of CarProduct Xn by A7;
ex pxi be Point of ElmFin(X,n+1) st pxi=px.(n+1) by A22; then
reconsider z = px.(n+1) as Point of Xn1;
PtCarProduct px = [y,z] by Th4;
hence x is Point of CarProduct X by A22,Th10;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A6);
hence thesis;
end;
theorem Th17:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X, px be n-element FinSequence st
x = PtCarProduct px holds
(for i be non zero Nat st i <= n holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i)
proof
let n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X, px be n-element FinSequence;
assume
A1: x = PtCarProduct px;
consider py be n-element FinSequence such that
A2: x = PtCarProduct py
& for i be non zero Nat st i <= n holds
ex pyi be Point of ElmFin(X,i) st pyi = py.i by Th16;
px = py by A1,A2,Th5;
hence thesis by A2;
end;
theorem Th18:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x,y be Point of CarProduct X, px,py be n-element FinSequence st
x = PtCarProduct px & y = PtCarProduct py holds
ex pxy be n-element FinSequence st x+y = PtCarProduct pxy
proof
defpred P[non zero Nat] means
for X be $1-element RealNormSpace-Sequence,
x,y be Point of CarProduct X, px,py be $1-element FinSequence st
x = PtCarProduct px & y = PtCarProduct py holds
ex pxy be $1-element FinSequence st x+y = PtCarProduct pxy;
A1: P[1]
proof
let X be 1-element RealNormSpace-Sequence;
set X1 = ElmFin(X,1);
ElmFin(X,1) = X.1 by Def3; then
A2: CarProduct X = X1 by Def4;
let x,y be Point of CarProduct X, px,py be 1-element FinSequence;
assume
A3: x = PtCarProduct px & y = PtCarProduct py;
A4: PtCarProduct px =px.1 by Def1;
ex pxi be Point of ElmFin(X,1) st pxi=px.1 by A3,Th17; then
reconsider px1=px.1 as Point of X1;
ex pyi be Point of ElmFin(X,1) st pyi=py.1 by A3,Th17; then
reconsider py1=py.1 as Point of X1;
reconsider pxy=<*px1+py1*> as 1-element FinSequence;
take pxy;
(PtProdFinSeq pxy).1 = pxy.1 by Def1;
hence thesis by A2,A3,A4,Def1;
end;
A5: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A6: P[n];
let X be (n+1)-element RealNormSpace-Sequence;
set Xn1 = SubFin(X,n);
set Xn11 = ElmFin(X,n+1);
A7: n <= n+1 by NAT_1:11;
A8: Xn1 = X|n & Xn11 = X.(n+1) by Def3,Def6,NAT_1:11;
A9: CarProduct X = [: CarProduct Xn1,Xn11 :] by Th10;
let x,y be Point of CarProduct X, px,py be (n+1)-element FinSequence;
assume
A10: x = PtCarProduct px & y = PtCarProduct py;
reconsider px1 = px|n as n-element FinSequence;
A11: PtCarProduct px = [ PtCarProduct px1,px.(n+1) ] by Th4;
for i be non zero Nat st i <= n holds
ex px1i be Point of ElmFin(Xn1,i) st px1i=px1.i
proof
let i be non zero Nat;
assume
A12: i <= n;
1 <= i by NAT_1:14; then
i in Seg n by A12; then
A13: Xn1.i = X.i & px1.i = px.i by A8,FUNCT_1:49;
ElmFin(X,i) = ElmFin(Xn1,i) by A7,A12,Th13;
hence thesis by A13,A7,A12,A10,Th17,XXREAL_0:2;
end; then
reconsider x1 = PtCarProduct px1 as Point of CarProduct Xn1 by Th16;
reconsider py1 = py|n as n-element FinSequence;
A14: PtCarProduct py = [ PtCarProduct py1,py.(n+1) ] by Th4;
for i be non zero Nat st i <= n holds
ex py1i be Point of ElmFin(Xn1,i) st py1i=py1.i
proof
let i be non zero Nat;
assume
A15: i <= n;
1 <= i by NAT_1:14; then
i in Seg n by A15; then
A16: Xn1.i = X.i & py1.i = py.i by A8,FUNCT_1:49;
ElmFin(X,i) = ElmFin(Xn1,i) by A7,A15,Th13;
hence thesis by A7,A15,A16,A10,Th17,XXREAL_0:2;
end; then
reconsider y1 = PtCarProduct py1 as Point of CarProduct Xn1 by Th16;
consider pxy1 be n-element FinSequence such that
A17: x1+y1 = PtCarProduct pxy1 by A6;
ex pxi be Point of ElmFin(X,n+1) st pxi = px.(n+1) by A10,Th17; then
reconsider pxn = px.(n+1) as Point of Xn11;
ex pyi be Point of ElmFin(X,n+1) st pyi = py.(n+1) by A10,Th17; then
reconsider pyn = py.(n+1) as Point of Xn11;
A18: x+y =[PtCarProduct(pxy1),pxn+pyn] by A10,A11,A14,A17,A9,PRVECT_3:18;
reconsider pxy = pxy1 ^ <*pxn+pyn*> as (n+1)-element FinSequence;
take pxy;
A19: len pxy1 = n by CARD_1:def 7; then
A20: pxy.(n+1) = pxn+pyn by FINSEQ_1:42;
dom pxy1 = Seg n by A19,FINSEQ_1:def 3; then
pxy1 = pxy|n by FINSEQ_1:21;
hence thesis by A20,A18,Th4;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A5);
hence thesis;
end;
theorem Th19:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x,y,z be Point of CarProduct X, px,py,pz be n-element FinSequence st
x = PtCarProduct px & y = PtCarProduct py & x+y = PtCarProduct pz holds
for i be non zero Nat st i <= n holds
ex pxi,pyi be Point of ElmFin(X,i) st
pxi = px.i & pyi = py.i & pxi + pyi = pz.i
proof
defpred P[non zero Nat] means
for X be $1-element RealNormSpace-Sequence,
x,y be Point of CarProduct X, px,py,pz be $1-element FinSequence st
x = PtCarProduct px & y = PtCarProduct py & x+y = PtCarProduct pz holds
for i be non zero Nat st i <= $1 holds
ex pxi,pyi be Point of ElmFin(X,i) st
pxi = px.i & pyi = py.i & pxi+pyi = pz.i;
A1: P[1]
proof
let X be 1-element RealNormSpace-Sequence;
set X1 = ElmFin(X,1);
ElmFin(X,1) = X.1 by Def3; then
A2: CarProduct X = X1 by Def4;
let x,y be Point of CarProduct X, px,py,pz be 1-element FinSequence;
assume
A3: x = PtCarProduct px & y = PtCarProduct py & x+y = PtCarProduct pz;
ex pxi be Point of ElmFin(X,1) st pxi=px.1 by A3,Th17; then
reconsider px1=px.1 as Point of X1;
ex pyi be Point of ElmFin(X,1) st pyi=py.1 by A3,Th17; then
reconsider py1=py.1 as Point of X1;
reconsider pxy=<*px1+py1*> as 1-element FinSequence;
ex pzi be Point of ElmFin(X,1) st pzi=pz.1 by A3,Th17; then
reconsider pz1 = pz.1 as Point of X1;
A4: x = px.1 & y = py.1 & x+y = pz.1 by A3,Def1;
hereby let i be non zero Nat;
assume
A5: i <= 1;
1 <= i by NAT_1:14; then
i = 1 by A5,XXREAL_0:1;
hence ex pxi,pyi be Point of ElmFin(X,i) st
pxi=px.i & pyi=py.i & pxi+pyi=pz.i by A2,A4;
end;
end;
A6: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A7: P[n];
let X be (n+1)-element RealNormSpace-Sequence;
set Xn1 = SubFin(X,n);
set Xn11 = ElmFin(X,n+1);
A8: n <= n+1 by NAT_1:11;
A9: Xn1 = X|n & Xn11 = X.(n+1) by Def6,Def3,NAT_1:11;
A10: CarProduct X =[: CarProduct Xn1,Xn11 :] by Th10;
let x,y be Point of CarProduct X, px,py,pz be (n+1)-element FinSequence;
assume
A11: x = PtCarProduct px & y = PtCarProduct py & x+y = PtCarProduct pz;
reconsider px1 = px|n as n-element FinSequence;
A12: PtCarProduct px = [ PtCarProduct px1,px.(n+1) ] by Th4;
for i be non zero Nat st i <= n holds
ex px1i be Point of ElmFin(Xn1,i) st px1i=px1.i
proof
let i be non zero Nat;
assume
A13: i <= n;
1 <= i by NAT_1:14; then
i in Seg n by A13; then
A14: Xn1.i = X.i & px1.i = px.i by A9,FUNCT_1:49;
ElmFin(X,i) = ElmFin(Xn1,i) by A8,A13,Th13;
hence thesis by A14,A8,A13,A11,Th17,XXREAL_0:2;
end; then
reconsider x1 = PtCarProduct px1 as Point of CarProduct Xn1 by Th16;
reconsider py1 = py|n as n-element FinSequence;
A15: PtCarProduct py = [ PtCarProduct py1,py.(n+1) ] by Th4;
for i be non zero Nat st i <= n holds
ex py1i be Point of ElmFin(Xn1,i) st py1i=py1.i
proof
let i be non zero Nat;
assume
A16: i <= n;
1 <= i by NAT_1:14; then
i in Seg n by A16; then
A17: Xn1.i = X.i & py1.i = py.i by A9,FUNCT_1:49;
ElmFin(X,i) = ElmFin(Xn1,i) by A8,A16,Th13;
hence thesis by A8,A16,A17,A11,Th17,XXREAL_0:2;
end; then
reconsider y1 = PtCarProduct py1 as Point of CarProduct Xn1 by Th16;
reconsider pz1 = pz|n as n-element FinSequence;
A18: PtCarProduct pz = [ PtCarProduct pz1,pz.(n+1) ] by Th4;
consider pxy1 be n-element FinSequence such that
A19: x1+y1 = PtCarProduct pxy1 by Th18;
ex pxi be Point of ElmFin(X,n+1) st pxi = px.(n+1) by A11,Th17; then
reconsider pxn = px.(n+1) as Point of Xn11;
ex pyi be Point of ElmFin(X,n+1) st pyi = py.(n+1) by A11,Th17; then
reconsider pyn = py.(n+1) as Point of Xn11;
x+y =[PtCarProduct(pxy1),pxn+pyn] by A11,A12,A15,A10,A19,PRVECT_3:18; then
A20: PtCarProduct pxy1 = PtCarProduct pz1 & pxn+pyn = pz.(n+1)
by A11,A18,XTUPLE_0:1; then
A21: pxy1 = pz1 by Th5;
hereby let i be non zero Nat;
assume
A22: i <= n+1;
A23: 1 <= i by NAT_1:14;
per cases;
suppose i <> n+1; then
i < n+1 by A22,XXREAL_0:1; then
A24: i <= n by NAT_1:13; then
A25: i in Seg n by A23;
A26: pz.i = pxy1.i by A21,A24,FINSEQ_3:112;
A27: px.i = px1.i & py.i = py1.i by FUNCT_1:49,A25;
ElmFin(X,i) = ElmFin(Xn1,i) by A8,A24,Th13;
hence ex pxi,pyi be Point of ElmFin(X,i)
st pxi=px.i & pyi=py.i & pxi+pyi=pz.i by A7,A19,A24,A26,A27;
end;
suppose i = n+1;
hence ex pxi,pyi be Point of ElmFin(X,i)
st pxi=px.i & pyi=py.i & pxi+pyi=pz.i by A20;
end;
end;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A6);
hence thesis;
end;
theorem Th20:
for n be non zero Nat, X be n-element RealNormSpace-Sequence, r be Real,
x be Point of CarProduct X, px be n-element FinSequence st
x = PtCarProduct px holds
ex prx be n-element FinSequence st r*x = PtCarProduct prx
proof
defpred P[non zero Nat] means
for X be $1-element RealNormSpace-Sequence, r be Real,
x be Point of CarProduct X, px be $1-element FinSequence st
x = PtCarProduct px holds
ex prx be $1-element FinSequence st r*x = PtCarProduct prx;
A1: P[1]
proof
let X be 1-element RealNormSpace-Sequence;
set X1 = ElmFin(X,1);
ElmFin(X,1) = X.1 by Def3; then
A2: CarProduct X = X1 by Def4;
let r be Real, x be Point of CarProduct X, px be 1-element FinSequence;
assume
A3: x = PtCarProduct px; then
ex pxi be Point of ElmFin(X,1) st pxi=px.1 by Th17; then
reconsider px1=px.1 as Point of X1;
reconsider prx=<*r*px1*> as 1-element FinSequence;
take prx;
(PtProdFinSeq prx).1 = prx.1 by Def1;
hence thesis by A2,A3,Def1;
end;
A4: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A5: P[n];
let X be (n+1)-element RealNormSpace-Sequence;
set n1 = n+1;
set Xn1 = SubFin(X,n);
set Xn11 = ElmFin(X,n+1);
A6: n <= n+1 by NAT_1:11;
A7: Xn1 = X|n & Xn11 = X.(n+1) by Def6,Def3,NAT_1:11;
A8: CarProduct X = [: CarProduct Xn1,Xn11 :] by Th10;
let r be Real, x be Point of CarProduct X,
px be (n+1)-element FinSequence;
assume
A9: x = PtCarProduct px;
reconsider px1 = px|n as n-element FinSequence;
A10: PtCarProduct(px) = [ PtCarProduct px1,px.(n+1) ] by Th4;
for i be non zero Nat st i <= n holds
ex px1i be Point of ElmFin(Xn1,i) st px1i=px1.i
proof
let i be non zero Nat;
assume
A11: i <= n;
1 <= i by NAT_1:14; then
i in Seg n by A11; then
A12: Xn1.i = X.i & px1.i = px.i by A7,FUNCT_1:49;
ElmFin(Xn1,i) = ElmFin(X,i) by A6,A11,Th13;
hence thesis by A9,A12,A6,A11,Th17,XXREAL_0:2;
end; then
reconsider x1 = PtCarProduct px1 as Point of CarProduct Xn1 by Th16;
consider prx1 be n-element FinSequence such that
A13: r*x1 = PtCarProduct prx1 by A5;
ex pxi be Point of ElmFin(X,n+1) st pxi=px.(n+1) by A9,Th17; then
reconsider pxn = px.(n+1) as Point of Xn11;
A14: r*x = [ PtCarProduct(prx1),r*pxn ] by A10,A9,A13,A8,PRVECT_3:18;
reconsider prx = prx1 ^ <*r*pxn*> as (n+1)-element FinSequence;
take prx;
A15: len prx1 = n by CARD_1:def 7; then
A16: prx.(n+1)=r*pxn by FINSEQ_1:42;
dom prx1 = Seg n by A15,FINSEQ_1:def 3; then
prx1 = prx|n by FINSEQ_1:21;
hence thesis by A16,A14,Th4;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A4);
hence thesis;
end;
theorem Th21:
for n be non zero Nat, X be n-element RealNormSpace-Sequence, r be Real,
x be Point of CarProduct X, px,prx be n-element FinSequence st
x = PtCarProduct px & r*x = PtCarProduct prx holds
for i be non zero Nat st i <= n holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i & r*pxi=prx.i
proof
defpred P[non zero Nat] means
for X be $1-element RealNormSpace-Sequence, r be Real,
x be Point of CarProduct X, px,prx be $1-element FinSequence st
x = PtCarProduct px & r*x = PtCarProduct prx holds
for i be non zero Nat st i <= $1 holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i & r*pxi=prx.i;
A1: P[1]
proof
let X be 1-element RealNormSpace-Sequence;
set X1 = ElmFin(X,1);
ElmFin(X,1) = X.1 by Def3; then
A2: CarProduct X = X1 by Def4;
let r be Real, x be Point of CarProduct X,
px,prx be 1-element FinSequence;
assume
A3: x = PtCarProduct px & r*x = PtCarProduct prx; then
ex pxi be Point of ElmFin(X,1) st pxi=px.1 by Th17; then
reconsider px1=px.1 as Point of X1;
ex prxi be Point of ElmFin(X,1) st prxi=prx.1 by A3,Th17; then
reconsider prx1 = prx.1 as Point of X1;
A4: x = px.1 & r*x = prx.1 by A3,Def1;
A5: now let i be non zero Nat;
assume
A6: i <= 1;
1 <= i by NAT_1:14; then
i = 1 by A6,XXREAL_0:1;
hence ex pxi be Point of ElmFin(X,i) st pxi=px.i & r*pxi = prx.i
by A2,A4;
end;
thus thesis by A5;
end;
A7: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A8: P[n];
let X be (n+1)-element RealNormSpace-Sequence;
set n1 = n+1;
set Xn1 = SubFin(X,n);
set Xn11 = ElmFin(X,n+1);
A9: n <= n+1 by NAT_1:11;
A10: Xn1 = X|n & Xn11 = X.(n+1) by Def6,Def3,NAT_1:11;
A11: CarProduct X = [: CarProduct Xn1,Xn11 :] by Th10;
let r be Real, x be Point of CarProduct X,
px,prx be (n+1)-element FinSequence;
assume
A12: x = PtCarProduct px & r*x = PtCarProduct prx;
reconsider px1 = px|n as n-element FinSequence;
A13: PtCarProduct(px) = [ PtCarProduct px1,px.(n+1) ] by Th4;
for i be non zero Nat st i <= n holds
ex px1i be Point of ElmFin(Xn1,i) st px1i=px1.i
proof
let i be non zero Nat;
assume
A14: i <= n;
1 <= i by NAT_1:14; then
i in Seg n by A14; then
A15: Xn1.i = X.i & px1.i = px.i by A10,FUNCT_1:49;
ElmFin(Xn1,i) = ElmFin(X,i) by A9,A14,Th13;
hence thesis by A12,A15,A9,A14,Th17,XXREAL_0:2;
end; then
reconsider x1 = PtCarProduct px1 as Point of CarProduct Xn1 by Th16;
reconsider prx1 = prx|n as n-element FinSequence;
A16: PtCarProduct prx = [ PtCarProduct prx1,prx.(n+1) ] by Th4;
consider prx2 be n-element FinSequence such that
A17: r*x1 = PtCarProduct prx2 by Th20;
ex pxi be Point of ElmFin(X,n+1) st pxi=px.(n+1) by A12,Th17; then
reconsider pxn = px.(n+1) as Point of Xn11;
r*x = [ PtCarProduct(prx2),r*pxn ] by A13,A12,A17,A11,PRVECT_3:18; then
A18: PtCarProduct prx1 = PtCarProduct prx2 & prx.(n+1) = r*pxn
by A12,A16,XTUPLE_0:1;
for i be non zero Nat st i <= n+1 holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i & r*pxi=prx.i
proof
let i be non zero Nat;
assume
A19: i <= n+1;
A20: 1 <= i by NAT_1:14;
per cases;
suppose i <> n+1; then
i < n+1 by A19,XXREAL_0:1; then
A21: i <= n by NAT_1:13; then
A22: i in Seg n by A20;
A23: prx.i = prx1.i by A21,FINSEQ_3:112;
A24: px.i = px1.i by A22,FUNCT_1:49;
ElmFin(X,i) = ElmFin(Xn1,i) by A9,A21,Th13;
hence ex pxi be Point of ElmFin(X,i) st pxi=px.i & r*pxi=prx.i
by A8,A17,A18,A21,A23,A24;
end;
suppose i = n+1;
hence ex pxi be Point of ElmFin(X,i) st pxi=px.i & r*pxi=prx.i by A18;
end;
end;
hence thesis;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A7);
hence thesis;
end;
theorem Th22:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X, px be n-element FinSequence st
x = PtCarProduct px holds
ex prx be n-element FinSequence st -x = PtCarProduct prx
proof
let n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X, px be n-element FinSequence;
assume x = PtCarProduct px; then
consider prx be n-element FinSequence such that
A1: (-1)*x = PtCarProduct prx by Th20;
take prx;
thus thesis by A1,RLVECT_1:16;
end;
theorem Th23:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X, px,pmx be n-element FinSequence st
x = PtCarProduct px & -x = PtCarProduct pmx holds
for i be non zero Nat st i <= n holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i & -pxi=pmx.i
proof
let n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X, px,pmx be n-element FinSequence;
assume
A1: x = PtCarProduct px & -x = PtCarProduct pmx;
A2: -x = (-1)*x by RLVECT_1:16;
hereby let i be non zero Nat;
assume i <= n; then
consider pxi be Point of ElmFin(X,i) such that
A3: pxi=px.i & (-1)*pxi=pmx.i by A1,A2,Th21;
take pxi;
thus pxi=px.i & -pxi=pmx.i by A3,RLVECT_1:16;
end;
end;
theorem Th24:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x,y be Point of CarProduct X, px,py be n-element FinSequence st
x = PtCarProduct px & y = PtCarProduct py holds
ex pxy be n-element FinSequence st x-y = PtCarProduct pxy
proof
let n be non zero Nat, X be n-element RealNormSpace-Sequence,
x,y be Point of CarProduct X, px,py be n-element FinSequence;
assume
A1: x = PtCarProduct px & y = PtCarProduct py; then
ex pry be n-element FinSequence st -y = PtCarProduct pry by Th22;
hence thesis by A1,Th18;
end;
theorem Th25:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x,y be Point of CarProduct X, px,py,pxy be n-element FinSequence st
x = PtCarProduct px & y = PtCarProduct py & x-y = PtCarProduct pxy holds
for i be non zero Nat st i <= n holds
ex pxi,pyi be Point of ElmFin(X,i) st pxi=px.i & pyi=py.i & pxi-pyi=pxy.i
proof
let n be non zero Nat, X be n-element RealNormSpace-Sequence,
x,y be Point of CarProduct X, px,py,pxy be n-element FinSequence;
assume
A1: x = PtCarProduct px & y = PtCarProduct py & x-y = PtCarProduct pxy; then
consider pry be n-element FinSequence such that
A2: -y = PtCarProduct pry by Th22;
for i be non zero Nat st i <= n holds
ex pxi,pyi be Point of ElmFin(X,i) st pxi=px.i & pyi=py.i & pxi-pyi=pxy.i
proof
let i be non zero Nat;
assume
A3: i <= n; then
consider pxi be Point of ElmFin(X,i) such that
A4: pxi=px.i by A1,Th17;
consider pyi be Point of ElmFin(X,i) such that
A5: pyi=py.i & -pyi=pry.i by A1,A2,A3,Th23;
take pxi,pyi;
ex px2i,py2i be Point of ElmFin(X,i) st
px2i = px.i & py2i = pry.i & px2i + py2i = pxy.i by A1,A2,A3,Th19;
hence thesis by A4,A5;
end;
hence thesis;
end;
theorem Th26:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X, px be n-element FinSequence st
x = PtCarProduct px holds
ex nrx be Element of REAL n st
( for i be non zero Nat st i <= n holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i & nrx.i =||.pxi.|| )
& ||.x.|| = |.nrx.|
proof
defpred P[non zero Nat] means
for X be $1-element RealNormSpace-Sequence,
x be Point of CarProduct X, px be $1-element FinSequence st
x = PtCarProduct px holds
ex nrx be Element of REAL $1 st
( for i be non zero Nat st i <= $1 holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i & nrx.i =||.pxi.|| )
& ||.x.|| = |.nrx.|;
A1: P[1]
proof
let X be 1-element RealNormSpace-Sequence;
set X1 = ElmFin(X,1);
ElmFin(X,1) = X.1 by Def3; then
A2: CarProduct X = X1 by Def4;
let x be Point of CarProduct X, px be 1-element FinSequence;
assume
A3: x = PtCarProduct px; then
ex pxi be Point of ElmFin(X,1) st pxi=px.1 by Th17; then
reconsider px1=px.1 as Point of X1;
<*||.px1.||*> in 1 -tuples_on REAL by FINSEQ_2:98; then
reconsider nrx=<*||.px1.||*> as Element of REAL 1 by EUCLID:def 1;
take nrx;
A4: x = px1 by A3,Def1;
A5: |.nrx.| = |. ||.px1.|| .| by Lm3;
now let i be non zero Nat;
assume
A6: i <= 1;
1 <= i by NAT_1:14; then
i = 1 by A6,XXREAL_0:1;
hence ex pxi be Point of ElmFin(X,i) st pxi=px.i & nrx.i = ||.pxi.||;
end;
hence thesis by A5,A4,A2,COMPLEX1:43;
end;
A7: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A8: P[n];
let X be (n+1)-element RealNormSpace-Sequence;
set Xn = SubFin(X,n);
set Xn1 = ElmFin(X,n+1);
A9: n <= n+1 by NAT_1:11;
A10: Xn = X|n & Xn1 = X.(n+1) by Def6,Def3,NAT_1:11;
A11: CarProduct X = [: CarProduct Xn,Xn1 :] by Th10;
let x be Point of CarProduct X, px be (n+1)-element FinSequence;
assume
A12: x = PtCarProduct px;
reconsider px1 = px|n as n-element FinSequence;
A13: PtCarProduct px = [ PtCarProduct px1,px.(n+1) ] by Th4;
for i be non zero Nat st i <= n holds
ex px1i be Point of ElmFin(Xn,i) st px1i=px1.i
proof
let i be non zero Nat;
assume
A14: i <= n;
1 <= i by NAT_1:14; then
i in Seg n by A14; then
A15: Xn.i = X.i & px1.i = px.i by A10,FUNCT_1:49;
ElmFin(Xn,i) = ElmFin(X,i) by A9,A14,Th13;
hence thesis by A12,A15,A9,A14,Th17,XXREAL_0:2;
end; then
reconsider x1 = PtCarProduct px1 as Point of CarProduct Xn by Th16;
consider prx1 be Element of REAL n such that
A16: ( for i be non zero Nat st i <= n holds
ex px1i be Point of ElmFin(Xn,i) st px1i=px1.i & prx1.i = ||.px1i.|| )
& ||.x1.|| = |.prx1.| by A8;
ex pxi be Point of ElmFin(X,n+1) st pxi=px.(n+1) by A12,Th17; then
reconsider pxn = px.(n+1) as Point of Xn1;
consider w be Element of REAL 2 such that
A17: w = <* ||.x1.||,||.pxn.|| *> & ||.x.|| = |.w.| by A11,A13,A12,PRVECT_3:18;
reconsider pp = ||.pxn.|| as Element of REAL;
set qq = <*pp *>;
set prx = prx1 ^ <*pp *>;
A18: len prx1 = n by CARD_1:def 7;
len prx = n+1 by CARD_1:def 7; then
prx is Element of (n+1)-tuples_on REAL by FINSEQ_2:92; then
reconsider prx as Element of REAL (n+1) by EUCLID:def 1;
take prx;
for i be non zero Nat st i <= n+1 holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i & prx.i = ||.pxi.||
proof
let i be non zero Nat;
assume
A19: i <= n+1;
A20: 1 <= i by NAT_1:14;
per cases;
suppose i <> n+1; then
i < n+1 by A19,XXREAL_0:1; then
A21: i <= n by NAT_1:13; then
A22: i in Seg n by A20;
i in dom prx1 by A18,A20,A21,FINSEQ_3:25; then
A23: prx.i = prx1.i by FINSEQ_1:def 7;
A24: ex px1i be Point of ElmFin(Xn,i) st
px1i=px1.i & prx1.i =||.px1i.|| by A16,A21;
ElmFin(X,i) = ElmFin(Xn,i) by A21,A9,Th13;
hence ex pxi be Point of ElmFin(X,i) st pxi=px.i & prx.i = ||.pxi.||
by A22,A23,A24,FUNCT_1:49;
end;
suppose i = n+1;
hence ex pxi be Point of ElmFin(X,i) st pxi=px.i & prx.i =||.pxi.||;
end;
end;
hence thesis by A17,A16,Lm4;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A7);
hence thesis;
end;
definition
let n be non zero Nat, X be n-element RealNormSpace-Sequence;
func CarProd X -> Function of CarProduct X,product X means :Def7:
ex CX be non-empty n-element FinSequence st CX = carr X
& CarProduct CX = the carrier of CarProduct X
& it = CarProd CX & it is bijective;
existence
proof
consider CX be non-empty n-element FinSequence such that
A1: CarProduct CX = the carrier of CarProduct X & CX = carr X
& for i be non zero Nat st i <= n holds CX.i = the carrier of ElmFin(X,i)
by Th12;
A2: product X = NORMSTR(# product carr X,zeros X,[:addop X:],
[:multop X:], productnorm X #) by PRVECT_2:6; then
reconsider F = CarProd CX as Function of CarProduct X,product X by A1;
take F;
CarProd CX is bijective by MEASUR14:12;
hence thesis by A1,A2;
end;
uniqueness;
end;
theorem Th27:
for n be non zero Nat, X,X1 be RealNormSpace-Sequence st
n <= len X & X1 = X | n holds carr X1 = (carr X) | n
proof
let n be non zero Nat, X,X1 be RealNormSpace-Sequence;
set CX1 = (carr X) |n;
assume that
A1: n <= len X and
A2: X1 = X|n;
A3: len X1 = n & dom X1 = Seg n by A1,A2,FINSEQ_1:17;
len carr X = len X by PRVECT_1:def 11; then
A4: len CX1 = n & dom CX1 = Seg n by A1,FINSEQ_1:17;
len carr X1 = len X1 by PRVECT_1:def 11; then
A5: dom (carr X1) = dom CX1 by A3,A4,FINSEQ_1:def 3;
now let k be Nat;
assume
A6: k in dom CX1; then
A7: CX1.k = (carr X).k by A4,FUNCT_1:49;
Seg n c= Seg (len X) by FINSEQ_1:5,A1; then
reconsider j = k as Element of dom X by A4,A6,FINSEQ_1:def 3;
reconsider l = k as Element of dom X1 by A1,A2,A4,A6,FINSEQ_1:17;
(carr X).j = the carrier of X.j by PRVECT_1:def 11; then
(carr X).j = the carrier of X1.l by A2,A4,A6,FUNCT_1:49;
hence CX1.k = (carr X1).k by A7,PRVECT_1:def 11;
end;
hence thesis by A5;
end;
theorem Th28:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X holds
ex px be n-element FinSequence st x = PtCarProduct px & (CarProd X).x = px
proof
defpred P[non zero Nat] means
for X be $1-element RealNormSpace-Sequence, x be Point of CarProduct X
holds
ex px be $1-element FinSequence st
x = PtCarProduct px & (CarProd X).x = px;
A1: P[1]
proof
let X be 1-element RealNormSpace-Sequence;
let x be Point of CarProduct X;
set X1 = ElmFin(X,1);
consider px be 1-element FinSequence such that
A2: x= PtCarProduct px
& (for i be non zero Nat st i <= 1 holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i) by Th16;
ex pxi be Point of ElmFin(X,1) st pxi=px.1 by A2; then
reconsider px1=px.1 as Point of X1;
A3: PtCarProduct px = px.1 by Def1;
A4: len px = 1 by CARD_1:def 7;
take px;
consider CX be non-empty 1-element FinSequence such that
A5: CX = carr X
& CarProduct CX = the carrier of CarProduct X
& CarProd X = CarProd CX & CarProd X is bijective by Def7;
consider id1 be Function of CarProduct SubFin(CX,1),product SubFin(CX,1)
such that
A6: (Pt2FinSeq CX).1 = id1 & id1 is bijective
& for x be object st x in CarProduct SubFin(CX,1) holds id1.x = <*x*>
by MEASUR14:def 5;
A7: CarProd CX = id1 by A6,MEASUR14:def 6;
A8: len CX = 1 by FINSEQ_3:153;
SubFin(CX,1) = CX|1 by MEASUR13:def 5; then
SubFin(CX,1) = CX by A8,FINSEQ_1:58; then
(CarProd X).x = <*x*> by A5,A7,A6;
hence thesis by A4,A2,A3,FINSEQ_1:40;
end;
A9: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A10: P[n];
let X be (n+1)-element RealNormSpace-Sequence;
set Xn1 = SubFin(X,n);
set Xn11 = ElmFin(X,n+1);
n < n+1 by NAT_1:13; then
A11: Xn1 = X|n by Def6;
A12: Xn11 = X.(n+1) by Def3;
let x be Point of CarProduct X;
consider px be (n+1)-element FinSequence such that
A13: x = PtCarProduct px
& ( for i be non zero Nat st i <= n+1 holds
ex pxi be Point of ElmFin(X,i) st pxi = px.i ) by Th16;
take px;
consider CX be non-empty (n+1)-element FinSequence such that
A14: CX = carr X
& CarProduct CX = the carrier of CarProduct X
& CarProd X = CarProd CX & CarProd X is bijective by Def7;
consider CXn1 be non-empty n-element FinSequence such that
A15: CXn1 = carr Xn1
& CarProduct CXn1 = the carrier of CarProduct Xn1
& CarProd Xn1 = CarProd CXn1 & CarProd Xn1 is bijective by Def7;
A16: len X = n+1 & len Xn1 = n by CARD_1:def 7;
A17: n <= n+1 by NAT_1:13; then
A18: CXn1 = CX|n by A11,A15,A14,A16,Th27;
reconsider px1 = px|n as n-element FinSequence;
for i be non zero Nat st i <= n holds
ex px1i be Point of ElmFin(Xn1,i) st px1i = px1.i
proof
let i be non zero Nat;
assume
A19: i <= n;
1 <= i by NAT_1:14; then
i in Seg n by A19; then
A20: Xn1.i = X.i & px1.i = px.i by A11,FUNCT_1:49;
ElmFin(X,i) = X.i & ElmFin(Xn1,i) = Xn1.i by A17,A19,XXREAL_0:2,Def3;
hence thesis by A13,A20,A17,A19,XXREAL_0:2;
end; then
reconsider x1 =PtCarProduct px1 as Point of CarProduct Xn1 by Th16;
ex prx1 be n-element FinSequence st
x1 = PtCarProduct prx1 & (CarProd Xn1).x1 = prx1 by A10; then
A21: (CarProd CXn1).x1 = px1 by A15,Th5;
ex pxi be Point of ElmFin(X,n+1) st pxi=px.(n+1) by A13; then
reconsider pxn = px.(n+1) as Point of Xn11;
len px = n+1 by CARD_1:def 7; then
A22: px = px1 ^ <*px.(n+1)*> by FINSEQ_3:55;
A23: n+1 in Seg (n+1) by FINSEQ_1:4;
len X = n+1 by CARD_1:def 7; then
reconsider n1 = (n+1) as Element of dom X by A23,FINSEQ_1:def 3;
CX.n1 = the carrier of X.n1 by A14,PRVECT_1:def 11; then
pxn in CX.(n+1) by A12; then
A24: pxn in ElmFin(CX,n+1) by MEASUR13:def 1;
A25: CXn1 = SubFin(CX,n) by A17,A18,MEASUR13:def 5; then
ex s,t be FinSequence st
(CarProd SubFin(CX,n)).x1 = s & <*pxn*> = t
& (CarProd CX).(x1,pxn) = s^t by A15,A24,MEASUR14:13;
hence thesis by A13,A14,A25,A21,A22,Th4;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A9);
hence thesis;
end;
theorem Th29:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x,y be Point of CarProduct X holds
(CarProd X).(x+y) = (CarProd X).x + (CarProd X).y
proof
let n be non zero Nat, X be n-element RealNormSpace-Sequence;
let x,y be Point of CarProduct X;
consider px be n-element FinSequence such that
A1: x = PtCarProduct px & (CarProd X).x = px by Th28;
consider py be n-element FinSequence such that
A2: y = PtCarProduct py & (CarProd X).y = py by Th28;
consider qxy be n-element FinSequence such that
A3: x + y = PtCarProduct(qxy) by A1,A2,Th18;
A4: ex pxy be n-element FinSequence st
x+y = PtCarProduct pxy & (CarProd X).(x+y) = pxy by Th28;
A5: product X = NORMSTR(# product carr X,zeros X,[:addop X:],
[:multop X:], productnorm X #) by PRVECT_2:6; then
reconsider vx = (CarProd X).x, vy = (CarProd X).y
as Element of product carr X;
dom ( [:addop X:].(vx,vy) ) = dom carr X by CARD_3:9; then
A6: dom ( [:addop X:].(vx,vy) ) = Seg len (carr X ) by FINSEQ_1:def 3; then
A7: dom ( [:addop X:].(vx,vy) ) = Seg len X by PRVECT_1:def 11; then
A8: dom ( [:addop X:].(vx,vy) ) = Seg n by CARD_1:def 7;
dom qxy = Seg len qxy by FINSEQ_1:def 3; then
A9: dom qxy = Seg n by CARD_1:def 7;
now let k be object;
assume
A10: k in dom ([:addop X:].(vx,vy)); then
reconsider i = k as Element of dom carr X by CARD_3:9;
A11: ([:addop X:].(vx,vy)).i = (the addF of X.i).(vx.i,vy.i) by Lm1;
reconsider j = i as non zero Nat by A10,A6,FINSEQ_1:1;
A12: 1 <= j & j <= n by A10,A8,FINSEQ_1:1; then
ex pxj,pyj be Point of ElmFin(X,j) st
pxj = px.j & pyj = py.j & pxj + pyj = qxy.j by A1,A2,A3,Th19;
hence ([:addop X:].(vx,vy)).k = qxy.k by A1,A2,A11,A12,Def3;
end; then
([:addop X:].(vx,vy)) = qxy by A7,A9,CARD_1:def 7;
hence thesis by A4,A3,A5,Th5;
end;
theorem Th30:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X, r be Element of REAL holds
(CarProd X).(r*x) = r * (CarProd X).x
proof
let n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X, r be Element of REAL;
consider px be n-element FinSequence such that
A1: x = PtCarProduct px & (CarProd X).x = px by Th28;
consider qxy be n-element FinSequence such that
A2: r*x = PtCarProduct qxy by A1,Th20;
A3: ex pxy be n-element FinSequence st
r*x = PtCarProduct pxy & (CarProd X).(r*x) = pxy by Th28;
A4: product X = NORMSTR(# product carr X,zeros X,[:addop X:],
[:multop X:], productnorm X #) by PRVECT_2:6; then
reconsider vx = (CarProd X).x as Element of product carr X;
dom ([:multop X:].(r,vx)) = dom carr X by CARD_3:9; then
A5: dom ([:multop X:].(r,vx)) = Seg len (carr X ) by FINSEQ_1:def 3; then
dom ([:multop X:].(r,vx)) = Seg len X by PRVECT_1:def 11; then
A6: dom ([:multop X:].(r,vx)) = Seg n by CARD_1:def 7;
A7: dom qxy = Seg len qxy by FINSEQ_1:def 3;
now let k be object;
assume
A8: k in dom ([:multop X:].(r,vx)); then
reconsider i = k as Element of dom carr X by CARD_3:9;
reconsider j = i as non zero Nat by A5,A8,FINSEQ_1:1;
A9: ([:multop X:].(r,vx)).i = (the Mult of X.i).(r,vx.i) by Lm2;
A10: 1 <= i & i <= n by A6,A8,FINSEQ_1:1; then
ex pxj be Point of ElmFin(X,j) st pxj = px.j & r*pxj = qxy.j
by A1,A2,Th21;
hence ([:multop X:].(r,vx)).k = qxy.k by A1,A9,A10,Def3;
end; then
([:multop X:].(r,vx)) = qxy by A6,A7,CARD_1:def 7;
hence thesis by A4,A3,A2,Th5;
end;
theorem Th31:
for n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X holds ||. (CarProd X).x .|| = ||.x.||
proof
let n be non zero Nat, X be n-element RealNormSpace-Sequence,
x be Point of CarProduct X;
consider px be n-element FinSequence such that
A1: x = PtCarProduct px & (CarProd X).x = px by Th28;
consider nrx be Element of REAL n such that
A2: ( for i be non zero Nat st i <= n holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i & nrx.i =||.pxi.|| )
& ||.x.|| = |.nrx.| by Th26,A1;
product X = NORMSTR(# product carr X,zeros X,[:addop X:],
[:multop X:], productnorm X #) by PRVECT_2:6; then
reconsider vx = (CarProd X).x as Element of product carr X;
len nrx = n by CARD_1:def 7; then
A3: dom nrx = Seg n by FINSEQ_1:def 3;
normsequence(X,vx) in REAL(len X); then
normsequence(X,vx) in (len X) -tuples_on REAL by EUCLID:def 1; then
normsequence(X,vx) in { s where s is Element of REAL * : len s = len X }
by FINSEQ_2:def 4; then
A4: ex s be Element of REAL* st s= normsequence(X,vx) & len s = len X; then
len normsequence(X,vx) = n by CARD_1:def 7; then
A5: dom normsequence(X,vx) = Seg n by FINSEQ_1:def 3;
now let k be object;
assume
A6: k in dom normsequence(X,vx); then
reconsider i = k as non zero Nat by A5,FINSEQ_1:1;
k in Seg len X by A4,A6,FINSEQ_1:def 3; then
reconsider j = k as Element of dom X by FINSEQ_1:def 3;
A7: normsequence(X,vx).k = (the normF of X.j).(vx.j) by PRVECT_2:def 11;
A8: i <= n by A5,A6,FINSEQ_1:1; then
ex pxi be Point of ElmFin(X,i) st pxi=px.i & nrx.i = ||.pxi.|| by A2;
hence (normsequence(X,vx)).k = nrx.k by A1,A7,A8,Def3;
end; then
nrx = normsequence(X,vx) by A3,A5;
hence thesis by A2,PRVECT_2:7;
end;
begin :: Product space of real normed spaces
Lm6:
for n be non zero Nat, X be non empty set holds
Seg n --> X is non-empty n-element FinSequence
proof
let n be non zero Nat, X be non empty set;
set Xn = Seg n --> X;
A1: dom Xn = Seg n & rng Xn = {X} by FUNCOP_1:8;
reconsider Xn as FinSequence;
n is Element of NAT by ORDINAL1:def 12; then
len Xn = n by A1,FINSEQ_1:def 3;
hence thesis by CARD_1:def 7;
end;
registration
let n be non zero Nat, X be non empty set;
cluster Seg n --> X -> non-empty n-element for FinSequence;
correctness by Lm6;
end;
registration
let n be non zero Nat;
cluster Seg n --> RNS_Real -> n-element non empty RealNormSpace-yielding
for FinSequence;
correctness
proof
set X = Seg n --> RNS_Real;
A1: for x being set st x in rng X holds x is RealNormSpace
proof
let x be set;
assume x in rng X; then
ex i be object st i in dom X & x=X.i by FUNCT_1:def 3;
hence thesis by FUNCOP_1:7;
end;
A2: n is Element of NAT by ORDINAL1:def 12;
dom X = Seg n; then
len X = n by FINSEQ_1:def 3,A2;
hence thesis by A1,CARD_1:def 7,PRVECT_2:def 10;
end;
end;
theorem Th32:
for n be non zero Nat, u be object holds
u is Point of CarProduct(Seg n--> RNS_Real) iff
ex pu be n-element FinSequence of RNS_Real st u = PtCarProduct pu
proof
let n be non zero Nat, u be object;
set X = Seg n --> RNS_Real;
hereby assume
u is Point of CarProduct(Seg n--> RNS_Real); then
consider pu be n-element FinSequence such that
A1: u = PtCarProduct pu
& ( for i be non zero Nat st i <= n holds
ex pui be Point of ElmFin(X,i) st pui=pu.i ) by Th16;
now let y be object;
assume y in rng pu; then
consider i be object such that
A2: i in dom pu & y=pu.i by FUNCT_1:def 3;
reconsider i as Nat by A2;
A3: dom pu = Seg len pu by FINSEQ_1:def 3; then
reconsider i as non zero Nat by A2,FINSEQ_1:1;
A4: dom pu = Seg n by A3,CARD_1:def 7; then
A5: i <= n by A2,FINSEQ_1:1; then
A6: ex pui be Point of ElmFin(X,i) st pui = pu.i by A1;
A7: ElmFin(X,i) = (Seg n --> RNS_Real).i by A5,Def3;
(Seg n --> RNS_Real).i = RNS_Real by FUNCOP_1:7,A2,A4;
hence y in the carrier of RNS_Real by A2,A6,A7;
end; then
rng pu c= the carrier of RNS_Real; then
reconsider pu as n-element FinSequence of RNS_Real by FINSEQ_1:def 4;
u = PtCarProduct pu by A1;
hence ex pu be n-element FinSequence of RNS_Real st u = PtCarProduct pu;
end;
assume
ex pu be n-element FinSequence of RNS_Real st u= PtCarProduct pu; then
consider pu be n-element FinSequence of RNS_Real such that
A8: u= PtCarProduct pu;
for i be non zero Nat st i <= n holds
ex pui be Point of ElmFin(X,i) st pui=pu.i
proof
let i be non zero Nat;
assume
A9: i <= n;
1 <= i by NAT_1:14; then
A10: i in Seg n by A9; then
A11: (Seg n --> RNS_Real).i = RNS_Real by FUNCOP_1:7;
i in Seg len pu by A10,CARD_1:def 7; then
i in dom pu by FINSEQ_1:def 3; then
pu.i in rng pu by FUNCT_1:3; then
reconsider pui = pu.i as Point of ElmFin(X,i) by A11,A9,Def3;
take pui;
thus thesis;
end;
hence u is Point of CarProduct(Seg n--> RNS_Real) by A8,Th16;
end;
Lm7:
for n be non zero Nat, a be n-element FinSequence of REAL, r be Real st 0 < r
ex D1 be non-empty n-element FinSequence st
for i be Nat st i in Seg n holds D1.i = ].a.i-r,a.i+r.[
proof
let n be non zero Nat,
a be n-element FinSequence of REAL,
r be Real;
assume A1: 0 < r;
defpred P[Nat,object] means ex y be Real st y = a.$1 & $2 = ].y-r,y+r.[;
A2: for k be Nat st k in Seg n ex x be object st P[k,x]
proof
let k be Nat;
assume k in Seg n;
reconsider y=a.k as Real;
take x = ].y-r,y+r.[;
thus thesis;
end;
consider D1 be FinSequence such that
A3: dom D1 = Seg n
& for k be Nat st k in Seg n holds P[k,D1.k] from FINSEQ_1:sch 1(A2);
n is Element of NAT by ORDINAL1:def 12; then
len D1 =n by A3,FINSEQ_1:def 3; then
reconsider D1 as n-element FinSequence by CARD_1:def 7;
A4: for i be Nat st i in Seg n holds D1.i = ].a.i-r,a.i+r.[
proof
let i be Nat;
assume i in Seg n; then
ex y be Real st y =a.i & D1.i = ].y-r,y+r.[ by A3;
hence thesis;
end;
not {} in rng D1
proof
assume {} in rng D1; then
consider i be object such that
A5: i in dom D1 & {} = D1.i by FUNCT_1:def 3;
reconsider i as Nat by A5;
A6: a.i-r < a.i - 0 by A1,XREAL_1:15;
a.i+0 < a.i +r by A1,XREAL_1:8; then
a.i in ].a.i-r,a.i+r.[ by A6;
hence contradiction by A3,A4,A5;
end; then
reconsider D1 as non-empty n-element FinSequence by RELAT_1:def 9;
take D1;
thus thesis by A4;
end;
theorem Th33:
for n be non zero Nat, D be non-empty n-element FinSequence,
px be n-element FinSequence holds
PtCarProduct px in CarProduct D
iff for i be Nat st i in Seg n holds px.i in D.i
proof
let n be non zero Nat, D be non-empty n-element FinSequence,
px be n-element FinSequence;
hereby assume PtCarProduct px in CarProduct D; then
consider py be n-element FinSequence such that
A1: py in product D & PtCarProduct px = PtCarProduct py by Th6;
px = py by A1,Th5; then
consider g be Function such that
A2: px = g & dom g = dom D
& for i being object st i in dom D holds g.i in D.i by A1,CARD_3:def 5;
dom D = Seg len D by FINSEQ_1:def 3; then
dom D = Seg n by CARD_1:def 7;
hence for i being Nat st i in Seg n holds px.i in D.i by A2;
end;
assume
A3: for i being Nat st i in Seg n holds px.i in D.i;
dom D = Seg len D by FINSEQ_1:def 3; then
A4: dom D = Seg n by CARD_1:def 7; then
A5:for i being object st i in dom D holds px.i in D.i by A3;
dom px = Seg len px by FINSEQ_1:def 3; then
dom px = Seg n by CARD_1:def 7; then
px in product D by A4,A5,CARD_3:def 5;
hence PtCarProduct px in CarProduct D by Th6;
end;
theorem Th34:
for n be non zero Nat, D be non-empty n-element FinSequence st
for i be Nat st i in Seg n holds D.i c= REAL
holds CarProduct D c= CarProduct(Seg n --> REAL)
proof
let n be non zero Nat, D be non-empty n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds D.i c= REAL;
now let x be object;
assume x in CarProduct D; then
consider px be n-element FinSequence such that
A2: px in product D & x = PtCarProduct px by Th6;
consider g be Function such that
A3: px = g & dom g = dom D
& for i being object st i in dom D holds g.i in D.i by A2,CARD_3:def 5;
dom D = Seg len D by FINSEQ_1:def 3; then
A4: dom D = dom(Seg n--> REAL) by CARD_1:def 7;
for i being object st i in dom (Seg n--> REAL) holds
g.i in (Seg n--> REAL).i
proof
let i be object;
assume
A5: i in dom (Seg n--> REAL); then
reconsider j = i as Nat;
D.j c= REAL by A1,A5; then
g.i in REAL by A3,A4,A5;
hence g.i in (Seg n--> REAL).i by A5,FUNCOP_1:7;
end; then
px in product (Seg n -->REAL) by A3,A4,CARD_3:def 5;
hence x in CarProduct(Seg n--> REAL) by A2,Th6;
end;
hence thesis;
end;
theorem Th35:
for n be non zero Nat holds CarProduct(Seg n --> RAT) is countable
proof
defpred P[non zero Nat] means CarProduct(Seg $1 --> RAT) is countable;
A1: P[1]
proof
set D = Seg 1 --> RAT;
A2: 1 in Seg 1;
CarProduct D = D.1 by MEASUR13:def 3;
hence thesis by A2,FUNCOP_1:7;
end;
A3: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A4: P[n];
set D = Seg (n+1) --> RAT;
A5: n <= n+1 by NAT_1:13; then
A6: SubFin(D,n) = D|n & ElmFin(D,n+1) = D.(n+1)
by MEASUR13:def 1,def 5;
CarProduct D = [: CarProduct SubFin(D,n),ElmFin(D,n+1) :]
by MEASUR13:6; then
A7: CarProduct D = [: CarProduct SubFin(D,n),RAT :]
by A6,FUNCOP_1:7,FINSEQ_1:3;
D|n = (Seg (n+1) /\ Seg n)--> RAT by FUNCOP_1:12; then
D|n = Seg n --> RAT by A5,FINSEQ_1:5,XBOOLE_1:28;
hence CarProduct D is countable by A6,A4,A7,CARD_4:7;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A3);
hence thesis;
end;
Lm8:
for n be non zero Nat, a be n-element FinSequence of REAL, r be Real st 0 < r
ex b be n-element FinSequence of RAT st
for i be Nat st i in Seg n holds b.i in ].a.i-r,a.i+r.[
proof
let n be non zero Nat, a be n-element FinSequence of REAL, r be Real;
assume
A1: 0 < r;
defpred P[Nat,object] means
ex y be Rational st $2 = y & y in ].a.$1-r,a.$1+r.[;
A2: for i be Nat st i in Seg n ex x be object st P[i,x]
proof
let i be Nat;
assume i in Seg n;
a.i-r < a.i & a.i < a.i+r by A1,XREAL_1:29,44; then
a.i-r < a.i+r by XXREAL_0:2; then
consider qx be Rational such that
A3: a.i-r < qx & qx < a.i+r by RAT_1:7;
take qx;
qx in ].a.i-r,a.i+r.[ by A3;
hence thesis;
end;
consider b be FinSequence such that
A4: dom b = Seg n
& for k be Nat st k in Seg n holds P[k,b.k] from FINSEQ_1:sch 1(A2);
n is Element of NAT by ORDINAL1:def 12; then
len b = n by A4,FINSEQ_1:def 3; then
reconsider b as n-element FinSequence by CARD_1:def 7;
A5: for i be Nat st i in Seg n holds b.i in ].a.i-r,a.i+r.[
proof
let i be Nat;
assume i in Seg n; then
ex y be Rational st b.i =y & y in ].a.i-r,a.i+r.[ by A4;
hence thesis;
end;
now let y be object;
assume y in rng b; then
consider i be object such that
A6: i in dom b & y = b.i by FUNCT_1:def 3;
reconsider i as Nat by A6;
ex z be Rational st b.i = z & z in ].a.i-r,a.i+r.[ by A4,A6;
hence y in RAT by A6,RAT_1:def 2;
end; then
rng b c= RAT; then
reconsider b as n-element FinSequence of RAT by FINSEQ_1:def 4;
take b;
thus thesis by A5;
end;
Lm10:
for n be non zero Nat, a,x be n-element FinSequence of REAL
ex r be Real st 0 < r
& for i be Nat st i in Seg n holds x.i in ].a.i-r,a.i+r.[
proof
let n be non zero Nat, a,x be n-element FinSequence of REAL;
defpred P[Nat,object] means
ex r be Real st $2=r & 0 < r & x.$1 in ].a.$1-r,a.$1+r.[;
A1: for i be Nat st i in Seg n ex x be object st P[i,x]
proof
let i be Nat;
assume i in Seg n;
ex r1 be Real st 0 <r1 & x.i in ].a.i-r1,a.i+r1.[ by Lm9;
hence thesis;
end;
consider R be FinSequence such that
A2: dom R = Seg n
& for k be Nat st k in Seg n holds P[k,R.k] from FINSEQ_1:sch 1(A1);
n is Element of NAT by ORDINAL1:def 12; then
len R = n by A2,FINSEQ_1:def 3; then
reconsider R as n-element FinSequence by CARD_1:def 7;
now let y be object;
assume y in rng R; then
consider i be object such that
A3: i in dom R & y = R.i by FUNCT_1:def 3;
reconsider i as Nat by A3;
ex r be Real st R.i=r & 0 < r & x.i in ].a.i-r,a.i+r.[ by A2,A3;
hence y in REAL by A3,XREAL_0:def 1;
end; then
rng R c= REAL; then
reconsider R as n-element FinSequence of REAL by FINSEQ_1:def 4;
reconsider G = rng R as finite Subset of REAL;
A4:for i be Nat st i in Seg n holds R.i <= upper_bound G
proof
let i be Nat;
assume i in Seg n; then
R.i in rng R by A2,FUNCT_1:3;
hence R.i <= upper_bound G by SEQ_4:def 1;
end;
1 <= n by NAT_1:14; then
A5:1 in Seg n; then
A6:ex r be Real st R.1 =r & 0 < r & x.1 in ].a.1-r,a.1+r.[ by A2;
take r = upper_bound G;
thus 0 < r by A4,A5,A6;
let i be Nat;
assume
A7:i in Seg n; then
A8: ].a.i-R.i,a.i+R.i.[ c= ].a.i-r,a.i+r.[ by A4,INTEGRA6:2;
ex r be Real st R.i = r & 0 < r & x.i in ]. a.i-r,a.i+r .[ by A2,A7;
hence x.i in ].a.i-r,a.i+r.[ by A8;
end;
theorem Th36:
for n be non zero Nat holds Prod_Measure(L-Meas n) is sigma_finite
proof
let n be non zero Nat;
set X = Seg n --> REAL;
set S = L-Field n;
set m = L-Meas n;
for i being Nat st i in Seg n
ex Xi be non empty set, Fi being SigmaField of Xi,
mi be sigma_Measure of Fi
st Xi=X.i & Fi = S.i & mi=m.i & mi is sigma_finite
proof
let i be Nat;
assume
A1: i in Seg n;
A2: REAL = X.i by A1,FUNCOP_1:7;
S = Seg n --> L-Field by MEASUR14:def 9; then
A3: L-Field = S.i by A1,FUNCOP_1:7;
m = Seg n --> L-Meas by MEASUR14:def 10; then
m.i = L-Meas by A1,FUNCOP_1:7;
hence thesis by A2,A3,MESFUN16:5;
end;
hence thesis by MEASUR13:29,def 15;
end;
theorem
for n be non zero Nat holds
Prod_Measure(Prod_Measure(L-Meas n),L-Meas) is sigma_finite
proof
let n be non zero Nat;
Prod_Measure(L-Meas n) is sigma_finite by Th36;
hence thesis by MEASUR13:27,MESFUN16:5;
end;
theorem
for n be 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
let n be non zero Nat;
set R1 = SubFin(Seg(n+1)--> REAL,n);
set S1 = SubFin(Seg(n+1)--> RNS_Real,n);
A1: n < n+1 by NAT_1:13; then
A2: R1 = (Seg (n+1) --> REAL) |n
& ElmFin(Seg(n+1) --> REAL,n+1) = (Seg(n+1)--> REAL).(n+1)
by MEASUR13:def 1,def 5; then
CarProduct(Seg (n+1) --> REAL)
= [:CarProduct R1,(Seg (n+1) --> REAL).(n+1):] by MEASUR13:6; then
A3: CarProduct(Seg(n+1) --> REAL) = [: CarProduct R1,REAL :]
by FUNCOP_1:7,FINSEQ_1:3;
A4: Seg n c= Seg (n+1) by FINSEQ_1:5,NAT_1:11;
(Seg (n+1) --> REAL) |n = (Seg (n+1) /\ Seg n)--> REAL by FUNCOP_1:12;
hence CarProduct(Seg (n+1) --> REAL)
= [: CarProduct(Seg n --> REAL),REAL :] by A2,A3,A4,XBOOLE_1:28;
S1 = (Seg (n+1) --> RNS_Real) |n by A1,Def6; then
S1 = (Seg(n+1) /\ Seg n) --> RNS_Real by FUNCOP_1:12; then
A5: S1 = Seg n --> RNS_Real by A4,XBOOLE_1:28;
ElmFin(Seg(n+1) --> RNS_Real,n+1) = (Seg(n+1)--> RNS_Real).(n+1)
by Def3; then
ElmFin(Seg(n+1) --> RNS_Real,n+1) = RNS_Real by FUNCOP_1:7,FINSEQ_1:3;
hence thesis by A5,Th10;
end;
theorem Th39:
for n be non zero Nat, D be non-empty n-element FinSequence st
for i be 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
defpred P[non zero Nat] means
for D be non-empty $1-element FinSequence st
for i be Nat st i in Seg $1 holds D.i is Element of L-Field
holds CarProduct D is Element of Prod_Field(L-Field $1);
A1: P[1]
proof
let D be non-empty 1-element FinSequence;
assume
A2: for i be Nat st i in Seg 1 holds D.i is Element of L-Field;
1 in Seg 1; then
D.1 is Element of L-Field by A2;
hence CarProduct D is Element of Prod_Field(L-Field 1)
by MEASUR13:def 3,MEASUR14:41;
end;
A3: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A4: P[n];
let D be non-empty (n+1)-element FinSequence;
assume
A5: for i be Nat st i in Seg (n+1) holds D.i is Element of L-Field;
set D1 = SubFin(D,n);
A6: n < n+1 by NAT_1:13; then
A7: D1 = D|n & ElmFin(D,n+1) = D.(n+1) by MEASUR13:def 1,def 5;
for i be Nat st i in Seg n holds D1.i is Element of L-Field
proof
let i be Nat;
assume
A8: i in Seg n;
Seg n c= Seg(n+1) by A6,FINSEQ_1:5; then
D.i is Element of L-Field by A5,A8;
hence thesis by A7,A8,FUNCT_1:49;
end; then
A9: CarProduct D1 is Element of Prod_Field(L-Field n) by A4;
D.(n+1) is Element of L-Field by A5,FINSEQ_1:3; then
A10: [: CarProduct D1,D.(n+1) :]
in measurable_rectangles(Prod_Field(L-Field n),L-Field) by A9;
set X = Seg (n+1) --> REAL;
set S = L-Field (n+1);
X|n = Seg (n+1) /\ Seg n --> REAL by FUNCOP_1:12; then
A11: X|n = Seg n --> REAL by A6,FINSEQ_1:5,XBOOLE_1:28;
A12: X.(n+1) = REAL by FINSEQ_1:3,FUNCOP_1:7;
A13: S = Seg(n+1) --> L-Field by MEASUR14:def 9; then
S|n = Seg (n+1) /\ Seg n --> L-Field by FUNCOP_1:12; then
S|n = Seg n --> L-Field by A6,FINSEQ_1:5,XBOOLE_1:28; then
A14: S|n = L-Field n by MEASUR14:def 9;
A15: S.(n+1) = L-Field by A13,FINSEQ_1:3,FUNCOP_1:7;
A16: SubFin(X,n) = X|n & ElmFin(X,n+1) = X.(n+1)
by A6,MEASUR13:def 1,def 5;
SubFin(S,n) = S|n & ElmFin(S,n+1) = S.(n+1)
by A6,MEASUR13:def 6,def 7; then
A17: Prod_Field S
= sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by A16,A12,A11,A14,A15,MEASUR13:34;
measurable_rectangles (Prod_Field(L-Field n),L-Field)
c= sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by PROB_1:def 9;
hence thesis by A7,A17,A10,MEASUR13:6;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A3);
hence thesis;
end;
theorem Th40:
for n be non zero Nat holds
CarProduct(Seg n -->REAL) in Prod_Field(L-Field n)
proof
let n be non zero Nat;
now let i be Nat;
assume i in Seg n; then
(Seg n -->REAL).i = REAL by FUNCOP_1:7;
hence (Seg n -->REAL).i is Element of L-Field by PROB_1:5;
end; then
CarProduct(Seg n -->REAL) is Element of Prod_Field(L-Field n) by Th39;
hence thesis;
end;
theorem
for n be non zero Nat, D be non-empty n-element FinSequence st
for i be Nat st i in Seg n holds D.i is Interval holds
CarProduct D is Element of Prod_Field(L-Field n)
proof
defpred P[non zero Nat] means
for D be non-empty $1-element FinSequence st
for i be Nat st i in Seg $1 holds D.i is Interval holds
CarProduct D is Element of Prod_Field(L-Field $1);
A1: P[1]
proof
let D be non-empty 1-element FinSequence;
assume
A2: for i be Nat st i in Seg 1 holds D.i is Interval;
1 in Seg 1; then
D.1 is Interval by A2; then
D.1 is Element of L-Field by MEASUR10:5,MEASUR12:75;
hence CarProduct D is Element of Prod_Field(L-Field 1)
by MEASUR13:def 3,MEASUR14:41;
end;
A3: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A4: P[n];
let D be non-empty (n+1)-element FinSequence;
assume
A5: for i be Nat st i in Seg (n+1) holds D.i is Interval;
set D1 = SubFin(D,n);
A6: n < n+1 by NAT_1:13; then
A7: D1 = D|n & ElmFin(D,n+1) = D.(n+1) by MEASUR13:def 1,def 5;
A8: Seg n c= Seg (n+1) by A6,FINSEQ_1:5;
for i be Nat st i in Seg n holds D1.i is Interval
proof
let i be Nat;
assume
A9 : i in Seg n; then
i <= n by FINSEQ_1:1; then
D1.i = D.i by A7,FINSEQ_3:112;
hence thesis by A5,A8,A9;
end; then
A10: CarProduct D1 is Element of Prod_Field(L-Field n) by A4;
set X = Seg (n+1) --> REAL;
set S = L-Field (n+1);
X|n = Seg (n+1) /\ Seg n -->REAL by FUNCOP_1:12; then
A11: X|n = Seg n --> REAL by A6,FINSEQ_1:5,XBOOLE_1:28;
A12: X.(n+1) = REAL by FINSEQ_1:3,FUNCOP_1:7;
A13: S = Seg (n+1) --> L-Field by MEASUR14:def 9; then
S|n = Seg (n+1) /\ Seg n --> L-Field by FUNCOP_1:12; then
S|n = Seg n --> L-Field by A6,FINSEQ_1:5,XBOOLE_1:28; then
A14: S|n = L-Field n by MEASUR14:def 9;
A15: S.(n+1) = L-Field by A13,FINSEQ_1:3,FUNCOP_1:7;
A16: n < n+1 by NAT_1:13; then
A17: SubFin(X,n) = X|n & ElmFin(X,n+1) = X.(n+1) by MEASUR13:def 1,def 5;
A18: SubFin(S,n) = S|n & ElmFin(S,n+1) = S.(n+1) by A16,MEASUR13:def 6,def 7;
A19: Prod_Field S = sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by A17,A18,A12,A11,A14,A15,MEASUR13:34;
D.(n+1) is Interval by A5,FINSEQ_1:3; then
D.(n+1) in L-Field by MEASUR10:5,MEASUR12:75; then
A20: [:CarProduct D1,D.(n+1):]
in measurable_rectangles(Prod_Field(L-Field n),L-Field) by A10;
measurable_rectangles (Prod_Field(L-Field n),L-Field)
c= sigma measurable_rectangles (Prod_Field(L-Field n),L-Field)
by PROB_1:def 9;
hence thesis by A20,A7,A19,MEASUR13:6;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A3);
hence thesis;
end;
theorem Th42:
for n be non zero Nat holds
the carrier of CarProduct(Seg n--> RNS_Real) = CarProduct(Seg n--> REAL)
proof
let n be non zero Nat;
set X = (Seg n --> RNS_Real);
consider CX be non-empty n-element FinSequence such that
A1: CarProduct CX = the carrier of CarProduct X & CX = carr X
& for i be non zero Nat st i <= n holds CX.i = the carrier of ElmFin(X,i)
by Th12;
A2: dom CX = Seg len CX by FINSEQ_1:def 3; then
A3: dom CX = Seg n by CARD_1:def 7;
A4: dom (Seg n --> REAL) = Seg n;
now let k be Nat;
assume
A5: k in dom CX; then
reconsider k1 = k as Element of dom X by A2,CARD_1:def 7;
(Seg n --> RNS_Real).k = RNS_Real by A3,A5,FUNCOP_1:7; then
CX.k1 = the carrier of RNS_Real by A1,PRVECT_1:def 11;
hence CX.k = (Seg n --> REAL).k;
end;
hence thesis by A1,A3,A4,FINSEQ_1:13;
end;
theorem Th43:
for n be non zero Nat, px be n-element FinSequence of REAL holds
px in product (Seg n--> REAL)
proof
let n be non zero Nat, px be n-element FinSequence of REAL;
set f = Seg n--> REAL;
dom px = Seg len px by FINSEQ_1:def 3; then
A1: dom px = Seg n by CARD_1:def 7;
for y being object st y in dom f holds px.y in f.y
proof
let y be object;
assume
A2: y in dom f; then
A3: f.y = REAL by FUNCOP_1:7;
px.y in rng px by A2,A1,FUNCT_1:3;
hence thesis by A3;
end;
hence thesis by A1,CARD_3:def 5;
end;
theorem Th44:
for n be non zero Nat, px be n-element FinSequence of RAT holds
px in product (Seg n--> RAT)
proof
let n be non zero Nat, px be n-element FinSequence of RAT;
set f = Seg n--> RAT;
dom px = Seg len px by FINSEQ_1:def 3; then
A1: dom px = Seg n by CARD_1:def 7;
for y being object st y in dom f holds px.y in f.y
proof
let y be object;
assume
A2: y in dom f; then
A3: f.y = RAT by FUNCOP_1:7;
rng px c= RAT by FINSEQ_1:def 4;
hence thesis by A3,A1,A2,FUNCT_1:3;
end;
hence thesis by A1,CARD_3:def 5;
end;
theorem Th45:
for n be non zero Nat, x be object holds
x in CarProduct(Seg n--> REAL) iff
ex px be n-element FinSequence of REAL st x = PtCarProduct px
proof
let n be non zero Nat, x be object;
hereby assume
A1: x in CarProduct(Seg n--> REAL);
consider px be n-element FinSequence such that
A2: px in product (Seg n--> REAL) & x = PtCarProduct px by A1,Th6;
now let y be object;
assume y in rng px; then
consider i be object such that
A3: i in dom px & y = px.i by FUNCT_1:def 3;
dom px = Seg len px by FINSEQ_1:def 3; then
A4: dom px = Seg n by CARD_1:def 7;
ex g be Function st px = g & dom g = dom (Seg n--> REAL)
& for i being object st i in dom (Seg n--> REAL) holds
g.i in (Seg n--> REAL).i by A2,CARD_3:def 5; then
px.i in (Seg n--> REAL).i by A3;
hence y in REAL by A3,A4,FUNCOP_1:7;
end; then
rng px c= REAL; then
reconsider px as n-element FinSequence of REAL by FINSEQ_1:def 4;
x = PtCarProduct px by A2;
hence ex px be n-element FinSequence of REAL st x = PtCarProduct px;
end;
given px be n-element FinSequence of REAL such that
A5: x = PtCarProduct px;
px in product (Seg n--> REAL) by Th43;
hence x in CarProduct(Seg n--> REAL) by A5,Th6;
end;
theorem Th46:
for n be non zero Nat, x be object holds
x in CarProduct(Seg n--> RAT) iff
ex px be n-element FinSequence of RAT st x = PtCarProduct px
proof
let n be non zero Nat, x be object;
hereby assume
A1: x in CarProduct(Seg n--> RAT);
consider px be n-element FinSequence such that
A2: px in product (Seg n--> RAT) & x = PtCarProduct px by A1,Th6;
now let y be object;
assume y in rng px; then
consider i be object such that
A3: i in dom px & y = px.i by FUNCT_1:def 3;
dom px = Seg len px by FINSEQ_1:def 3; then
A4: dom px = Seg n by CARD_1:def 7;
ex g be Function st px = g & dom g = dom (Seg n--> RAT)
& for i being object st i in dom (Seg n--> RAT)
holds g.i in (Seg n--> RAT).i by A2,CARD_3:def 5; then
px.i in (Seg n--> RAT).i by A3;
hence y in RAT by A3,A4,FUNCOP_1:7;
end; then
rng px c= RAT; then
reconsider px as n-element FinSequence of RAT by FINSEQ_1:def 4;
x = PtCarProduct px by A2;
hence ex px be n-element FinSequence of RAT st x = PtCarProduct px;
end;
assume ex px be n-element FinSequence of RAT st x = PtCarProduct px; then
consider px be n-element FinSequence of RAT such that
A5: x = PtCarProduct px;
px in product (Seg n--> RAT) by Th44;
hence x in CarProduct(Seg n--> RAT) by A5,Th6;
end;
theorem
for n be non zero Nat, x be object st x in CarProduct(Seg n--> REAL)
ex px be n-element FinSequence of REAL
st px in product(Seg n--> REAL) & x = PtCarProduct px
proof
let n be non zero Nat, x be object;
assume x in CarProduct(Seg n--> REAL); then
ex px be n-element FinSequence of REAL st x = PtCarProduct px by Th45;
hence thesis by Th43;
end;
theorem Th48:
for n be non zero Nat, X,Y be non-empty n-element FinSequence st
for i be Nat st i in Seg n holds X.i c= Y.i
holds CarProduct X c= CarProduct Y
proof
let n be non zero Nat, X,Y be non-empty n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds X.i c= Y.i;
now let x be object;
assume x in CarProduct X; then
consider px be n-element FinSequence such that
A2: px in product X & x = PtCarProduct px by Th6;
consider g be Function such that
A3: px = g & dom g = dom X
& for i being object st i in dom X holds g.i in X.i by A2,CARD_3:def 5;
dom X = Seg len X by FINSEQ_1:def 3; then
A4: dom X = Seg n by CARD_1:def 7;
dom Y = Seg len Y by FINSEQ_1:def 3; then
A5: dom Y = Seg n by CARD_1:def 7;
for i being object st i in dom Y holds g.i in Y.i
proof
let i be object;
assume
A6: i in dom Y; then
reconsider j=i as Nat;
X.j c= Y.j by A1,A6,A5;
hence g.i in Y.i by A6,A5,A4,A3;
end; then
px in product Y by A3,A4,A5,CARD_3:def 5;
hence x in CarProduct Y by A2,Th6;
end;
hence thesis;
end;
theorem Th49:
for n be non zero Nat holds
CarProduct(Seg n --> RAT) c= CarProduct(Seg n -->REAL)
proof
let n be non zero Nat;
now let i be Nat;
assume
A1: i in Seg n; then
(Seg n --> RAT).i = RAT by FUNCOP_1:7;
hence (Seg n --> RAT).i c= (Seg n --> REAL).i by A1,NUMBERS:12,FUNCOP_1:7;
end;
hence thesis by Th48;
end;
theorem
for n be non zero Nat, X be non empty set,
D be non-empty n-element FinSequence st
for i be Nat st i in Seg n holds D.i is Subset of X
holds CarProduct D is Subset of CarProduct(Seg n --> X)
proof
let n be non zero Nat, X be non empty set,
D be non-empty n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds D.i is Subset of X;
now let i be Nat;
assume
A2: i in Seg n; then
(Seg n --> X).i = X by FUNCOP_1:7; then
D.i is Subset of (Seg n --> X).i by A1,A2;
hence D.i c= (Seg n --> X).i;
end;
hence CarProduct D is Subset of CarProduct(Seg n --> X) by Th48;
end;
theorem Th51:
for n be non zero Nat, D be non-empty n-element FinSequence st
for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL
holds ex E be Subset of CarProduct(Seg n-->RNS_Real) st
E = CarProduct D & E is compact
proof
defpred P[non zero Nat] means
for D be non-empty $1-element FinSequence st
for i be Nat st i in Seg $1 holds D.i is closed_interval
Subset of REAL holds
ex E be Subset of CarProduct(Seg $1 --> RNS_Real)
st E = CarProduct D & E is compact;
A1: P[1]
proof
let D be non-empty 1-element FinSequence;
assume
A2: for i be Nat st i in Seg 1 holds D.i is closed_interval Subset of REAL;
A3: 1 in Seg 1; then
D.1 is closed_interval Subset of REAL by A2; then
consider a,b be Real such that
A4: D.1 = [. a,b .] by MEASURE5:def 3;
A5: CarProduct D = [. a,b .] by A4,MEASUR13:def 3;
set X = Seg 1 --> RNS_Real;
A6: CarProduct X = X.1 by Def4; then
A7: CarProduct X = RNS_Real by FUNCOP_1:7,A3;
reconsider E = CarProduct D as Subset of CarProduct X
by A3,A5,A6,FUNCOP_1:7;
take E;
thus E = CarProduct D;
set S = CarProduct X;
for u1 be sequence of S st rng u1 c= E
ex u2 be sequence of S st
u2 is subsequence of u1 & u2 is convergent & lim u2 in E
proof
let u1 be sequence of S;
assume
A8: rng u1 c= E;
reconsider s1 = u1 as Real_Sequence by A3,A6,FUNCOP_1:7;
consider s2 being Real_Sequence such that
A9: s2 is subsequence of s1 & s2 is convergent & lim s2 in [. a,b .]
by A5,A8,RCOMP_1:def 3,6;
consider N1 being increasing sequence of NAT such that
A10: s2 = s1 * N1 by A9,VALUED_0:def 17;
reconsider u2 = u1*N1 as sequence of S;
take u2;
thus u2 is subsequence of u1;
reconsider v2 = lim s2 as Point of S by A7,XREAL_0:def 1;
A11: for r be Real st 0 < r
ex m be Nat st for n be Nat st m <= n holds ||. (u2.n) - v2 .|| < r
proof
let r be Real;
assume 0 < r; then
consider m be Nat such that
A12: for n be Nat st m <= n holds |. (s2.n) - lim s2 .| < r
by A9,SEQ_2:def 7;
take m;
let n be Nat;
assume m <= n; then
A13: |. (s2.n) - lim s2 .| < r by A12;
reconsider xu2n = u2.n, xv = v2 as Point of RNS_Real
by A3,A6,FUNCOP_1:7;
xu2n -xv = s2.n -lim s2 by A10,DUALSP03:4;
hence ||.(u2.n) - v2.|| < r by A7,A13,EUCLID:def 2;
end; then
u2 is convergent;
hence thesis by A9,A5,A11,NORMSP_1:def 7;
end;
hence E is compact;
end;
A14:for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A15: P[n];
let D be non-empty (n+1)-element FinSequence;
assume
A16: for i be Nat st i in Seg (n+1) holds D.i is closed_interval
Subset of REAL;
set D1 = SubFin(D,n);
A17: n < n+1 by NAT_1:13; then
A18: D1 = D|n & ElmFin(D,n+1) = D.(n+1) by MEASUR13:def 5,def 1;
for i be Nat st i in Seg n holds D1.i is closed_interval Subset of REAL
proof
let i be Nat;
assume
A19: i in Seg n;
Seg n c= Seg (n+1) by A17,FINSEQ_1:5; then
D.i is closed_interval Subset of REAL by A16,A19;
hence thesis by A18,A19,FUNCT_1:49;
end; then
consider E1 be Subset of CarProduct(Seg n --> RNS_Real ) such that
A20: E1 = CarProduct D1 & E1 is compact by A15;
set n11 = n+1;
D.(n+1) is closed_interval Subset of REAL by A16,FINSEQ_1:3; then
consider a2,b2 be Real such that
A21: D.(n+1) = [. a2,b2 .] by MEASURE5:def 3;
reconsider E0 = [. a2,b2 .] as Subset of RNS_Real;
set S = RNS_Real;
for u1 be sequence of S st rng u1 c= E0
ex u2 be sequence of S st u2 is subsequence of u1 & u2 is convergent
& lim u2 in E0
proof
let u1 be sequence of S;
assume
A22: rng u1 c= E0;
reconsider s1=u1 as Real_Sequence;
consider s2 being Real_Sequence such that
A23: s2 is subsequence of s1 & s2 is convergent & lim s2 in [. a2,b2 .]
by A22,RCOMP_1:def 3,6;
consider N1 being increasing sequence of NAT such that
A24: s2 = s1 * N1 by A23,VALUED_0:def 17;
reconsider u2 = u1*N1 as sequence of S;
take u2;
thus u2 is subsequence of u1;
reconsider v2 = lim s2 as Point of S by XREAL_0:def 1;
A25: for r be Real st 0 < r
ex m be Nat st for n be Nat st m <= n holds ||. (u2.n) - v2.|| < r
proof
let r be Real;
assume 0 < r; then
consider m be Nat such that
A26: for n be Nat st m <= n holds |. (s2.n) - lim s2.| < r
by A23,SEQ_2:def 7;
take m;
let n be Nat;
assume m <= n; then
A27: |.(s2.n) - lim s2 .| < r by A26;
reconsider xu2n = u2.n, xv = v2 as Point of RNS_Real;
xu2n -xv = s2.n -lim s2 by A24,DUALSP03:4;
hence ||. (u2.n) - v2.|| < r by A27,EUCLID:def 2;
end; then
u2 is convergent;
hence thesis by A23,A25,NORMSP_1:def 7;
end; then
A28: E0 is compact;
set X = Seg (n+1) --> RNS_Real;
set Xn = SubFin(X,n), Xn1 = ElmFin(X,n+1);
A29: CarProduct X = [: CarProduct Xn,Xn1:] by Th10;
Xn1 = X.(n+1) by Def3; then
A30: Xn1 = RNS_Real by FUNCOP_1:7,FINSEQ_1:3;
Xn = X|n by A17,Def6; then
Xn = Seg (n+1) /\ Seg n --> RNS_Real by FUNCOP_1:12; then
A31: Xn = Seg n --> RNS_Real by A17,FINSEQ_1:5,XBOOLE_1:28; then
reconsider E = [:E1,E0:]
as Subset of CarProduct(Seg (n+1) --> RNS_Real) by A30,Th10;
take E;
thus thesis by A18,A20,A21,A28,A29,A30,A31,MEASUR13:6,MESFUN16:8;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A1,A14);
hence thesis;
end;
theorem
for n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py be n-element FinSequence of REAL st
x = PtCarProduct px & y = PtCarProduct py holds
ex pxy be n-element FinSequence of REAL st x+y = PtCarProduct pxy
proof
let n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py be n-element FinSequence of REAL;
assume
A1: x = PtCarProduct px & y = PtCarProduct py;
set X = Seg n --> RNS_Real;
consider pxy be n-element FinSequence such that
A2: x + y = PtCarProduct pxy by A1,Th18;
A3: dom pxy = Seg len pxy by FINSEQ_1:def 3; then
A4: dom pxy = Seg n by CARD_1:def 7;
now let y be object;
assume y in rng pxy; then
consider i be object such that
A5: i in dom pxy & y = pxy.i by FUNCT_1:def 3;
reconsider i as non zero Nat by A5,A3,FINSEQ_1:1;
A6: i <= n by A5,A4,FINSEQ_1:1; then
A7: ex pxi,pyi be Point of ElmFin(X,i) st
pxi=px.i & pyi=py.i & pxi+pyi=pxy.i by A1,A2,Th19;
X.i = RNS_Real by A5,A4,FUNCOP_1:7; then
ElmFin(X,i) = RNS_Real by A6,Def3;
hence y in REAL by A5,A7;
end; then
rng pxy c= REAL; then
reconsider pxy as n-element FinSequence of REAL by FINSEQ_1:def 4;
take pxy;
thus x+y = PtCarProduct pxy by A2;
end;
theorem
for n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py,pxy be n-element FinSequence of REAL st
x = PtCarProduct px & y = PtCarProduct py & x+y = PtCarProduct pxy holds
for i be Nat st i in Seg n holds pxy.i = px.i+py.i
proof
let n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py,pxy be n-element FinSequence of REAL;
assume
A1: x = PtCarProduct px & y = PtCarProduct py & x+y = PtCarProduct pxy;
set X = Seg n --> RNS_Real;
thus for i be Nat st i in Seg n holds pxy.i = px.i+py.i
proof
let i be Nat;
assume
A2: i in Seg n; then
reconsider i1=i as non zero Nat by FINSEQ_1:1;
A3: 1 <= i & i <= n by A2,FINSEQ_1:1; then
consider pxi,pyi be Point of ElmFin(X,i1) such that
A4: pxi=px.i & pyi=py.i & pxi+pyi=pxy.i by A1,Th19;
X.i =RNS_Real by A2,FUNCOP_1:7; then
ElmFin(X,i1) = RNS_Real by A3,Def3;
hence thesis by A4,BINOP_2:def 9;
end;
end;
theorem Th54:
for n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py be n-element FinSequence of REAL st
x = PtCarProduct px & y = PtCarProduct py holds
ex pxy be n-element FinSequence of REAL st x-y = PtCarProduct pxy
proof
let n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py be n-element FinSequence of REAL;
assume
A1: x = PtCarProduct px & y = PtCarProduct py;
set X = Seg n --> RNS_Real;
consider pxy be n-element FinSequence such that
A2:x-y = PtCarProduct pxy by A1,Th24;
A3:dom pxy = Seg len pxy by FINSEQ_1:def 3; then
A4:dom pxy = Seg n by CARD_1:def 7;
now let y be object;
assume y in rng pxy; then
consider i be object such that
A5: i in dom pxy & y = pxy.i by FUNCT_1:def 3;
reconsider i as non zero Nat by A5,A3,FINSEQ_1:1;
A6: i <= n by A5,A4,FINSEQ_1:1; then
consider pxi,pyi be Point of ElmFin(X,i) such that
A7: pxi=px.i & pyi=py.i & pxi-pyi=pxy.i by A1,A2,Th25;
X.i = RNS_Real by A5,A4,FUNCOP_1:7; then
ElmFin(X,i) = RNS_Real by A6,Def3;
hence y in REAL by A5,A7;
end; then
rng pxy c= REAL; then
reconsider pxy as n-element FinSequence of REAL by FINSEQ_1:def 4;
take pxy;
thus x-y = PtCarProduct pxy by A2;
end;
theorem Th55:
for n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py,pxy be n-element FinSequence of REAL st
x = PtCarProduct px & y = PtCarProduct py & x-y = PtCarProduct pxy holds
for i be Nat st i in Seg n holds pxy.i = px.i-py.i
proof
let n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py,pxy be n-element FinSequence of REAL;
assume
A1: x = PtCarProduct px & y = PtCarProduct py & x-y = PtCarProduct pxy;
set X = Seg n --> RNS_Real;
thus for i be Nat st i in Seg n holds pxy.i = px.i-py.i
proof
let i be Nat;
assume
A2: i in Seg n; then
reconsider i1=i as non zero Nat by FINSEQ_1:1;
A3: i <= n by A2,FINSEQ_1:1; then
A4: ex pxi,pyi be Point of ElmFin(X,i1) st
pxi=px.i & pyi=py.i & pxi-pyi=pxy.i by A1,Th25;
X.i =RNS_Real by A2,FUNCOP_1:7; then
ElmFin(X,i1) = RNS_Real by A3,Def3;
hence thesis by A4,DUALSP03:4;
end;
end;
theorem
for n be non zero Nat, x be Point of CarProduct(Seg n --> RNS_Real),
r be Real, px be n-element FinSequence of REAL st
x = PtCarProduct px holds
ex prx be n-element FinSequence of REAL st r*x = PtCarProduct prx
proof
let n be non zero Nat, x be Point of CarProduct(Seg n --> RNS_Real),
r be Real, px be n-element FinSequence of REAL;
assume
A1: x = PtCarProduct px;
set X = Seg n --> RNS_Real;
consider prx be n-element FinSequence such that
A2: r*x = PtCarProduct prx by A1,Th20;
A3: dom prx = Seg len prx by FINSEQ_1:def 3; then
A4: dom prx = Seg n by CARD_1:def 7;
now let y be object;
assume y in rng prx; then
consider i be object such that
A5: i in dom prx & y=prx.i by FUNCT_1:def 3;
reconsider i as non zero Nat by A5,A3,FINSEQ_1:1;
A6: i <= n by A5,A4,FINSEQ_1:1;
consider pxi be Point of ElmFin(X,i) such that
A7: pxi = px.i & r*pxi=prx.i by A6,A1,A2,Th21;
X.i = RNS_Real by A5,A4,FUNCOP_1:7; then
ElmFin(X,i) = RNS_Real by A6,Def3;
hence y in REAL by A5,A7;
end; then
rng prx c= REAL; then
reconsider prx as n-element FinSequence of REAL by FINSEQ_1:def 4;
take prx;
thus r*x= PtCarProduct(prx) by A2;
end;
theorem
for n be non zero Nat, x be Point of CarProduct(Seg n --> RNS_Real),
r be Real, px,prx be n-element FinSequence of REAL st
x = PtCarProduct px & r*x = PtCarProduct prx holds
for i be Nat st i in Seg n holds prx.i = r*px.i
proof
let n be non zero Nat, x be Point of CarProduct(Seg n --> RNS_Real),
r be Real, px,prx be n-element FinSequence of REAL;
assume
A1: x = PtCarProduct px & r*x = PtCarProduct prx;
set X = Seg n --> RNS_Real;
thus for i be Nat st i in Seg n holds prx.i = r*px.i
proof
let i be Nat;
assume
A2: i in Seg n; then
reconsider i1=i as non zero Nat by FINSEQ_1:1;
A3: i <= n by A2,FINSEQ_1:1; then
A4: ex pxi be Point of ElmFin(X,i1) st pxi=px.i & r*pxi=prx.i by A1,Th21;
X.i = RNS_Real by A2,FUNCOP_1:7; then
ElmFin(X,i1) = RNS_Real by A3,Def3;
hence thesis by A4,BINOP_2:def 11;
end;
end;
theorem Th58:
for n be non zero Nat, x be Point of CarProduct(Seg n --> RNS_Real),
px be n-element FinSequence of REAL st x = PtCarProduct px holds
ex nrx be Element of REAL n st
( for i be Nat st i in Seg n holds nrx.i = |.px.i.| ) & ||.x.|| = |.nrx.|
proof
let n be non zero Nat, x be Point of CarProduct(Seg n --> RNS_Real),
px be n-element FinSequence of REAL;
assume
A1: x = PtCarProduct px;
set X = Seg n --> RNS_Real;
consider nrx be Element of REAL n such that
A2: ( for i be non zero Nat st i <= n holds
ex pxi be Point of ElmFin(X,i) st pxi=px.i & nrx.i =||.pxi.|| )
& ||. x.|| = |.nrx.| by A1,Th26;
take nrx;
thus for i be Nat st i in Seg n holds nrx.i = |.px.i.|
proof
let i be Nat;
assume
A3: i in Seg n; then
reconsider i1=i as non zero Nat by FINSEQ_1:1;
A4: i <= n by A3,FINSEQ_1:1; then
A5: ex pxi be Point of ElmFin(X,i1) st pxi = px.i & nrx.i =||.pxi.|| by A2;
X.i = RNS_Real by A3,FUNCOP_1:7; then
ElmFin(X,i1) = RNS_Real by A4,Def3;
hence thesis by A5,EUCLID:def 2;
end;
thus ||.x.|| = |.nrx.| by A2;
end;
theorem Th59:
for n be non zero Nat, x be Point of CarProduct(Seg n --> RNS_Real),
px be n-element FinSequence of REAL, r be Real st
0 <= r & x = PtCarProduct px
& for i be Nat st i in Seg n holds |. px.i .| <= r/n holds ||.x.|| <= r
proof
let n be non zero Nat, x be Point of CarProduct(Seg n --> RNS_Real),
px be n-element FinSequence of REAL, r1 be Real;
assume
A1: 0 <= r1 & x = PtCarProduct px
& for i be Nat st i in Seg n holds |. px.i .| <= r1/n; then
consider nrx be Element of REAL n such that
A2: ( for i be Nat st i in Seg n holds nrx.i = |.px.i.| )
& ||.x.|| = |.nrx.| by Th58;
set r2 = r1/n;
r2*r2*n*1 <= r2*r2*n*n by A1,XREAL_1:64,NAT_1:14; then
r2*r2*n <= (r2*n)*(r2*n); then
r2*r2*n <= r1*(r2*n) by XCMPLX_1:87; then
r2*r2*n <= r1*r1 by XCMPLX_1:87; then
sqrt ((r2*r2)*n) <= sqrt(r1^2) by A1,SQUARE_1:26; then
A3: sqrt ((r2*r2)*n) <= r1 by A1,SQUARE_1:22;
for i being Nat st i in dom nrx holds 0 <= nrx.i & nrx.i <= r2
proof
let i be Nat;
assume i in dom nrx; then
i in Seg len nrx by FINSEQ_1:def 3; then
A4: i in Seg n by CARD_1:def 7; then
nrx.i = |.px.i.| by A2;
hence 0 <= nrx.i & nrx.i <= r2 by A4,A1;
end; then
|.nrx.| <= sqrt ((r2 * r2) * (len nrx)) by LOPBAN11:10; then
|.nrx.| <= sqrt ((r2 * r2) * n ) by CARD_1:def 7;
hence ||.x.|| <= r1 by A2,A3,XXREAL_0:2;
end;
Lm11:
for n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py be n-element FinSequence of REAL, r be Real st
0 <= r & x = PtCarProduct px & y = PtCarProduct py
& for i be Nat st i in Seg n holds |. px.i - py.i .| <= r/n
holds ||.x-y.|| <= r
proof
let n be non zero Nat, x,y be Point of CarProduct(Seg n --> RNS_Real),
px,py be n-element FinSequence of REAL, r1 be Real;
assume
A1: 0 <= r1 & x = PtCarProduct px & y = PtCarProduct py
& for i be Nat st i in Seg n holds |. px.i-py.i .| <= r1/n; then
consider pxy be n-element FinSequence of REAL such that
A2: x-y = PtCarProduct pxy by Th54;
for i be Nat st i in Seg n holds |. pxy.i .| <= r1/n
proof
let i be Nat;
assume
A3: i in Seg n; then
pxy.i = px.i-py.i by A1,A2,Th55;
hence |. pxy.i .| <= r1/n by A1,A3;
end;
hence thesis by A1,A2,Th59;
end;
begin :: Sigma finite measure on REAL n
theorem Th60:
for n be non zero Nat, A be set st
A c= CarProduct(Seg n --> REAL) & A /\ CarProduct(Seg n --> RAT) <> {} holds
ex p be sequence of CarProduct(Seg n --> REAL)
st rng p = A /\ CarProduct(Seg n --> RAT)
proof
let n be non zero Nat, A be set;
assume
A1: A c= CarProduct(Seg n --> REAL)
& A /\ CarProduct(Seg n --> RAT) <> {};
A /\ CarProduct(Seg n --> RAT) is countable by Th35,CARD_3:94; then
consider f being Function of omega,A /\ CarProduct(Seg n --> RAT) such that
A2: rng f = A /\ CarProduct(Seg n --> RAT) by CARD_3:96,A1;
A /\ CarProduct(Seg n --> RAT) c= A by XBOOLE_1:17; then
rng f c= CarProduct(Seg n --> REAL) by A1; then
reconsider f as sequence of CarProduct(Seg n --> REAL) by A1,FUNCT_2:6;
take f;
thus thesis by A2;
end;
theorem Th61:
for n be non zero Nat, D be non-empty n-element FinSequence,
px be n-element FinSequence holds
PtCarProduct px in CarProduct D iff
for i be Nat st i in Seg n holds px.i in D.i
proof
let n be non zero Nat, D be non-empty n-element FinSequence,
px be n-element FinSequence;
dom D = Seg len D by FINSEQ_1:def 3; then
A1: dom D = Seg n by CARD_1:def 7;
dom px = Seg len px by FINSEQ_1:def 3; then
A2:dom px = Seg n by CARD_1:def 7;
hereby assume PtCarProduct px in CarProduct D; then
consider py be n-element FinSequence such that
A3: py in product D & PtCarProduct px = PtCarProduct py by Th6;
px = py by A3,Th5; then
ex g be Function st
px = g & dom g = dom D
& for i being object st i in dom D holds g.i in D.i by A3,CARD_3:def 5;
hence for i being Nat st i in Seg n holds px.i in D.i by A1;
end;
assume for i being Nat st i in Seg n holds px.i in D.i; then
for i being object st i in dom D holds px.i in D.i by A1; then
px in product D by A1,A2,CARD_3:def 5;
hence PtCarProduct px in CarProduct D by Th6;
end;
theorem Th62:
for n be non zero Nat, r be Real,
f be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real
st f is_continuous_on dom f holds
ex H be Subset of CarProduct(Seg n --> RNS_Real)
st H /\ dom f = f"( ].-infty,r.[ ) & H is open
proof
let n be non zero Nat, r be Real,
f be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real;
assume
A1: f is_continuous_on dom f;
set E = dom f;
set S = CarProduct(Seg n --> RNS_Real);
A2: now let z be object;
assume
A3: z in f"( ].-infty,r.[ ); then
A4: z in dom f & f.z in ].-infty,r.[ by FUNCT_1:def 7; then
A5: ex t be Real st t = f.z & -infty < t & t < r;
reconsider t=z as Point of S by A3;
take t;
thus t=z;
reconsider y = f.t as Real;
set e = r-y;
consider s be Real such that
A6: 0<s
& for t1 be Point of S st t1 in E & ||. t1- t .|| < s
holds ||. f/.t1 - f/.t.|| < e by A1,A4,A5,XREAL_1:50,NFCONT_1:19;
take s;
thus 0<s by A6;
thus for t1 be object st
t1 in E/\ {t1 where t1 is Point of S : ||. t1- t .|| < s}
holds f.t1 in ].-infty,r.[
proof
let t1 be object;
assume
A7: t1 in E/\ {t1 where t1 is Point of S : ||. t1- t .|| < s}; then
A8: t1 in E & t1 in {t1 where t1 is Point of S : ||. t1- t .|| < s}
by XBOOLE_0:def 4;
reconsider y0=t1 as Point of S by A7;
A9: ex y1 be Point of S st y0=y1 & ||. y1- t .|| < s by A8;
reconsider r1=f/.y0, r2=f/.t as Real;
A10: r2 = f.t by A4,PARTFUN1:def 6;
f/.y0 - f/.t = r1-r2 by DUALSP03:4; then
||. f/.y0 - f/.t .|| = |.r1-r2.| by EUCLID:def 2; then
r1 in ].r2-e,r2+e.[ by A6,A8,A9,RCOMP_1:1; then
ex g be Real st g=r1 & r2-e < g & g < r2+ e; then
-infty < r1 & r1 < r by A10,XXREAL_0:12; then
r1 in ].-infty,r.[;
hence f.t1 in ].-infty,r.[ by A8,PARTFUN1:def 6;
end;
end;
defpred P[object,object] means
ex t be Point of S,s be Real st t=$1 & s=$2 & 0 < s
& for t1 be object st
t1 in E/\ {t1 where t1 is Point of S : ||. t1- t .|| < s}
holds f.t1 in ].-infty,r.[;
A11:for z being object st z in f"( ].-infty,r.[ )
ex y being object st y in REAL & P[z,y]
proof
let z be object;
assume z in f"( ].-infty,r.[ ); then
consider t be Point of S such that
A12: t = z
& ex s be Real st 0<s
& for t1 be object st
t1 in E/\ {t1 where t1 is Point of S : ||. t1- t .|| < s}
holds f.t1 in ].-infty,r.[ by A2;
consider s be Real such that
A13: 0 < s
& for t1 be object st
t1 in E/\ {t1 where t1 is Point of S : ||. t1- t .|| < s}
holds f.t1 in ].-infty,r.[ by A12;
reconsider y=s as Element of REAL by XREAL_0:def 1;
take y;
thus y in REAL;
thus thesis by A12,A13;
end;
consider R being Function of f"( ].-infty,r.[ ),REAL such that
A14:for x being object st x in f"( ].-infty,r.[ ) holds P[x,R.x]
from FUNCT_2:sch 1(A11);
defpred Q[object,object] means
ex t be Point of S st t=$1 & 0 < R.$1
& $2 = {t1 where t1 is Point of S : ||. t1- t .|| < R.$1};
A15:for z being object st z in f"( ].-infty,r.[ )
ex y being object st y in bool (the carrier of S) & Q[z,y]
proof
let z be object;
assume z in f"( ].-infty,r.[ ); then
consider t be Point of S,s be Real such that
A16: t=z & s=R.z & 0 < s
& for t1 be object st
t1 in E /\ {t1 where t1 is Point of S : ||. t1- t .|| < s}
holds f.t1 in ].-infty,r.[ by A14;
set y = {t1 where t1 is Point of S : ||. t1- t .|| < s};
take y;
now let x be object;
assume x in y; then
ex t1 be Point of S st x=t1 & ||. t1- t .|| < s;
hence x in the carrier of S;
end; then
y c= the carrier of S;
hence thesis by A16;
end;
consider B being Function of f"( ].-infty,r.[ ),bool (the carrier of S)
such that
A17:for x being object st x in f"( ].-infty,r.[ ) holds Q[x,B.x]
from FUNCT_2:sch 1(A15);
set H = union rng B;
reconsider H as Subset of CarProduct(Seg n --> RNS_Real);
take H;
for z be object holds z in H /\ E iff z in f"( ].-infty,r.[ )
proof
let z be object;
hereby assume z in H /\ E; then
A18: z in H & z in E by XBOOLE_0:def 4; then
consider Y being set such that
A19: z in Y & Y in rng B by TARSKI:def 4;
consider x be object such that
A20: x in dom B & Y=B.x by FUNCT_1:def 3,A19;
A21: ex t be Point of S st
t=x & 0 < R.x
& B.x = {t1 where t1 is Point of S : ||. t1- t .|| < R.x} by A17,A20;
A22: ex t be Point of S,s be Real st t=x & s=R.x & 0 < s
& for t1 be object st
t1 in E/\ {t1 where t1 is Point of S : ||. t1- t .|| < s}
holds f.t1 in ].-infty,r.[ by A14,A20;
z in E /\ (B.x) by A19,A20,A18,XBOOLE_0:def 4; then
f.z in ].-infty,r.[ by A21,A22;
hence z in f"( ].-infty,r.[ ) by A18,FUNCT_1:def 7;
end;
assume A23: z in f"( ].-infty,r.[ ); then
A24: z in E by FUNCT_1:def 7;
consider t be Point of S such that
A25: t=z & 0 < R.z
& B.z = {t1 where t1 is Point of S : ||. t1- t .|| < R.z } by A17,A23;
reconsider z0 =z as Point of S by A23;
||. z0- z0 .|| = ||. 0.S .|| by RLVECT_1:15; then
A26: z0 in B.z0 by A25;
z0 in dom B by A23,FUNCT_2:def 1; then
B.z0 in rng B by FUNCT_1:3; then
z in union rng B by A26,TARSKI:def 4;
hence z in H/\ E by A24,XBOOLE_0:def 4;
end;
hence H /\ E = f"( ].-infty,r.[ ) by TARSKI:2;
for z be Point of S st z in H holds ex N be Neighbourhood of z st N c= H
proof
let z be Point of S;
assume z in H; then
consider Y being set such that
A27: z in Y & Y in rng B by TARSKI:def 4;
consider x be object such that
A28: x in dom B & Y = B.x by FUNCT_1:def 3,A27;
consider t be Point of S such that
A29: t=x & 0 < R.x
& B.x = {t1 where t1 is Point of S : ||. t1- t .|| < R.x} by A17,A28;
A30: ex t1 be Point of S st z=t1 & ||. t1- t .|| < R.x by A29,A27,A28;
set e = R.x - ||. z- t .||;
reconsider N = {y where y is Point of S : ||. y- z .|| < e}
as Neighbourhood of z by A30,XREAL_1:50,NFCONT_1:3;
take N;
A31: now let p be object;
assume p in N; then
consider y be Point of S such that
A32: y = p & ||. y- z .|| < e;
A33: ||. y- t .|| <= ||. y- z .|| + ||.z-t.|| by NORMSP_1:10;
||. y- z .|| + ||.z-t.|| < e + ||.z-t.|| by A32,XREAL_1:8; then
||. y- t .|| < R.x by A33,XXREAL_0:2;
hence p in Y by A29,A28,A32;
end;
Y c= H by A27,ZFMISC_1:74;
hence N c= H by A31;
end;
hence H is open by NDIFF_1:5;
end;
Th63:
for n be non zero Nat, r be Real,
g be PartFunc of CarProduct(Seg n--> REAL),REAL holds
less_dom(g,r) = g"( ].-infty,r.[ ) by MESFUN16:17;
theorem Th65:
for n be non zero Nat, z being Point of CarProduct(Seg n--> RNS_Real),
r be Real st 0 < r holds
ex s be Real, x be n-element FinSequence of REAL,
D be non-empty n-element FinSequence
st 0 < s & s < r & z = PtCarProduct x
& (for i be Nat st i in Seg n holds D.i = ]. x.i-s,x.i+s .[)
& CarProduct D c= Ball(z,r)
proof
let n be non zero Nat, z be Point of CarProduct(Seg n--> RNS_Real),
r be Real;
assume
A1: 0 < r;
consider x be n-element FinSequence of RNS_Real such that
A2: z = PtCarProduct x by Th32;
reconsider x as n-element FinSequence of REAL;
reconsider s=(r/2)/n as Real;
A3: 0 < r/2 & r/2 < r by A1,XREAL_1:215,216; then
A4: 0 < s & s <= (r/2)/1 by XREAL_1:139,118,NAT_1:14;
consider D be non-empty n-element FinSequence such that
A5: for i be Nat st i in Seg n holds D.i = ]. x.i-s,x.i+s .[
by A3,Lm7,XREAL_1:139;
take s,x,D;
thus 0 < s & s < r & z=PtCarProduct x
& (for i be Nat st i in Seg n holds D.i = ]. x.i-s,x.i+s .[)
by A2,A3,A4,A5,XXREAL_0:2;
now let t be object;
assume
A6: t in CarProduct D;
for i be Nat st i in Seg n holds D.i c= REAL
proof
let i be Nat;
assume i in Seg n; then
D.i = ]. x.i-s,x.i+s .[ by A5;
hence thesis;
end; then
A7: CarProduct D c= CarProduct(Seg n -->REAL) by Th34; then
consider y be n-element FinSequence of REAL such that
A8: t = PtCarProduct y by A6,Th45;
reconsider u=t as Point of CarProduct(Seg n -->RNS_Real) by A6,A7,Th42;
now let i be Nat;
assume A9:i in Seg n; then
D.i = ]. x.i-s,x.i+s .[ by A5;
hence |. y.i -x.i .| <= s by A8,A6,A9,Th61,RCOMP_1:1;
end; then
||. u -z .|| <= r/2 by A2,A1,A8,Lm11; then
||. u -z .|| < r by A3,XXREAL_0:2; then
||. z -u .|| < r by NORMSP_1:7;
hence t in Ball(z,r);
end;
hence CarProduct D c= Ball(z,r);
end;
theorem Th66:
for n be non zero Nat, A be Subset of CarProduct(Seg n-->RNS_Real) st
A is open
& ( for a be n-element FinSequence of REAL st PtCarProduct a in A holds
ex Rx be real-membered set st
Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence
st ( for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[ )
& CarProduct D c= A} )
holds
ex F be Function of A,REAL st
for a be n-element FinSequence of REAL st PtCarProduct a in A holds
ex Rx be real-membered set st Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence
st ( for i be 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
let n be non zero Nat,
A be Subset of CarProduct(Seg n-->RNS_Real );
assume
A1: A is open
& for a be n-element FinSequence of REAL st PtCarProduct a in A holds
ex Rx be real-membered set st Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence st
( for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[ )
& CarProduct D c= A };
defpred P[object,object] means
ex a be n-element FinSequence of REAL, Rx be real-membered set st
$1 = PtCarProduct a
& Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence st
( for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[ )
& CarProduct D c= A}
& $2 = (upper_bound Rx)/2;
A2: for x being object st x in A ex y being object st y in REAL & P[x,y]
proof
let x be object;
assume
A3: x in A; then
x in the carrier of CarProduct(Seg n-->RNS_Real); then
x in CarProduct(Seg n-->REAL) by Th42; then
consider a be n-element FinSequence of REAL such that
A4: x = PtCarProduct a by Th45;
consider Rx be real-membered set such that
A5: Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence
st ( for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[ )
& CarProduct D c= A } by A1,A3,A4;
take y = (upper_bound Rx)/2;
thus y in REAL by XREAL_0:def 1;
thus thesis by A4,A5;
end;
consider F being Function of A,REAL such that
A6: for x being object st x in A holds P[x,F.x] from FUNCT_2:sch 1(A2);
take F;
thus for a be n-element FinSequence of REAL st PtCarProduct a in A holds
ex Rx be real-membered set st Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence
st ( for i be 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
let x be n-element FinSequence of REAL;
assume PtCarProduct x in A; then
consider a be n-element FinSequence of REAL, Rx be real-membered set
such that
A7: PtCarProduct x = PtCarProduct a
& Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence st
( for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[ )
& CarProduct D c= A }
& F.(PtCarProduct x) = (upper_bound Rx)/2 by A6;
x = a by A7,Th5;
hence thesis by A7;
end;
end;
theorem Th67:
for n be non zero Nat, A be Subset of CarProduct(Seg n --> RNS_Real)
st A is open holds A in Prod_Field(L-Field n)
proof
let n be non zero Nat, A be Subset of CarProduct(Seg n --> RNS_Real);
set S = Seg n --> RNS_Real;
set X = Seg n --> REAL;
assume
A1: A is open;
A2: the carrier of CarProduct S = CarProduct X by Th42;
per cases;
suppose A = {};
hence A in Prod_Field(L-Field n) by PROB_1:4;
end;
suppose
A3: A <> {};
per cases;
suppose
not (for a be n-element FinSequence of REAL st PtCarProduct a in A holds
ex Rx be real-membered set st Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence
st ( for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[ )
& CarProduct D c= A}); then
consider a be n-element FinSequence of REAL such that
A4: PtCarProduct a in A
& not
(ex Rx be real-membered set st Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[)
& CarProduct D c= A});
set Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[)
& CarProduct D c= A};
now let z be object;
assume z in Rx; then
ex r be Real st z=r & 0<r
& ex D be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[)
& CarProduct D c= A;
hence z is real;
end; then
reconsider Rx as real-membered set by MEMBERED:def 3;
reconsider x = PtCarProduct a as Point of CarProduct S by A4;
consider r0 being Real such that
A5: r0 > 0 & Ball (x,r0) c= A by A1,A4,NDIFF_8:20;
consider s be Real, aa be n-element FinSequence of REAL,
D be non-empty n-element FinSequence such that
A6: 0 < s & s < r0 & x=PtCarProduct aa
& (for i be Nat st i in Seg n holds D.i = ]. aa.i-s,aa.i+s .[)
& CarProduct D c= Ball(x,r0) by A5,Th65;
A7: aa = a by Th5,A6;
CarProduct D c= A by A6,A5; then
s in Rx by A6,A7; then
A8: not Rx is bounded_above by A4;
now let z be object;
assume z in CarProduct X; then
consider x be n-element FinSequence of REAL such that
A9: z = PtCarProduct x by Th45;
consider r be Real such that
A10: 0 < r
& for i be Nat st i in Seg n holds x.i in ].a.i-r,a.i+r.[ by Lm10;
not r is UpperBound of Rx by A8,XXREAL_2:def 10; then
consider s being ExtReal such that
A11: s in Rx & r < s by XXREAL_2:def 1;
reconsider s as Real by A11;
consider s0 be Real such that
A12: s = s0 & 0 < s0
& ex D be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds D.i = ].a.i-s0,a.i+s0.[)
& CarProduct D c= A by A11;
consider D be non-empty n-element FinSequence such that
A13: (for i be Nat st i in Seg n holds D.i = ].a.i-s0,a.i+s0.[)
& CarProduct D c= A by A12;
now let i be Nat;
assume
A14: i in Seg n;
].a.i-r,a.i+r.[ c= ].a.i-s,a.i+s.[ by A11,INTEGRA6:2; then
x.i in ].a.i-s,a.i+s.[ by A10,A14;
hence x.i in D.i by A14,A13,A12;
end;
hence z in A by A13,A9,Th33;
end; then
CarProduct X c= A; then
A = CarProduct X by A2;
hence thesis by Th40;
end;
suppose
for a be n-element FinSequence of REAL st PtCarProduct a in A holds
ex Rx be real-membered set st Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[)
& CarProduct D c= A}; then
consider F be Function of A,REAL such that
A15: for a be n-element FinSequence of REAL st PtCarProduct a in A holds
ex Rx be real-membered set st
Rx is non empty bounded_above
& Rx = {r where r is Real :0 < r
& ex D be non-empty n-element FinSequence st
(for i be 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 by A1,Th66;
A /\ CarProduct(Seg n --> RAT) <> {}
proof
consider z be object such that
A16: z in A by A3,XBOOLE_0:def 1;
reconsider u=z as Point of CarProduct S by A16;
consider e0 being Real such that
A17: e0 > 0 & Ball (u,e0) c= A by A16,A1,NDIFF_8:20;
set e=e0/4;
0 < e & e < e0 by A17,XREAL_1:223,224; then
A18: Ball (u,e) c= Ball (u,e0) by NDIFF_8:15; then
A19: 0 < e & Ball (u,e) c= A by A17,XREAL_1:224;
u in the carrier of CarProduct S; then
u in CarProduct X by Th42; then
consider xx be n-element FinSequence of REAL such that
A20: u = PtCarProduct xx by Th45;
reconsider ee = (e/2)/n as Real;
A21: 0 < e/2 & e/2 < e by A19,XREAL_1:215,216; then
consider qxx be n-element FinSequence of RAT such that
A22: for i be Nat st i in Seg n holds qxx.i in ].xx.i-ee,xx.i+ee.[
by Lm8,XREAL_1:139;
A23: PtCarProduct qxx in CarProduct(Seg n --> RAT) by Th46; then
PtCarProduct qxx in CarProduct X by Th49,TARSKI:def 3; then
reconsider v = PtCarProduct qxx as Point of CarProduct S by Th42;
rng qxx c= REAL; then
A24: qxx is n-element FinSequence of REAL by FINSEQ_1:def 4;
now let i be Nat;
assume i in Seg n; then
qxx.i in ].xx.i-ee,xx.i+ee.[ by A22;
hence |.qxx.i-xx.i.| <= ee by RCOMP_1:1;
end; then
||. v-u .|| <= e/2 by A24,A17,A20,Lm11; then
||. u-v .|| <=e/2 by NORMSP_1:7; then
||. u-v .|| < e by XXREAL_0:2,A21; then
v in Ball (u,e); then
PtCarProduct qxx in A by A18,A17;
hence A /\ CarProduct(Seg n --> RAT) <> {} by A23,XBOOLE_0:def 4;
end; then
consider p be sequence of CarProduct X such that
A25: rng p = A /\ CarProduct(Seg n --> RAT) by A2,Th60;
A26: for a be n-element FinSequence of REAL st PtCarProduct a in A
ex r be Real st 0< r & r = F.(PtCarProduct a)
& ex Da be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds Da.i = ].a.i-r,a.i+r.[)
& CarProduct Da c= A
proof
let a be n-element FinSequence of REAL;
assume PtCarProduct a in A; then
consider Rx be real-membered set such that
A27: Rx is non empty bounded_above
& Rx = {r where r is Real : 0 < r
& ex D be non-empty n-element FinSequence st
(for i be 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 by A15;
reconsider r0 = F.(PtCarProduct a) as Real;
take r0;
consider r1 be object such that
A28: r1 in Rx by A27;
reconsider r1 as Real by A28;
A29: ex r be Real st r1=r & 0 <r
& ex D be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[)
& CarProduct D c= A by A27,A28;
A30: r1 <= upper_bound Rx by SEQ_4:def 1,A27,A28; then
0 < r0 & r0 < upper_bound Rx by A27,A29,XREAL_1:215,216; then
consider s be Real such that
A31: s in Rx & (upper_bound Rx)-r0 < s by A27,SEQ_4:def 1;
consider r be Real such that
A32: s = r & 0 <r
& ex D be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[)
& CarProduct D c= A by A31,A27;
consider D be non-empty n-element FinSequence such that
A33: (for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[)
& CarProduct D c= A by A32;
consider Da be non-empty n-element FinSequence such that
A34: (for i be Nat st i in Seg n holds Da.i = ].a.i-r0,a.i+r0.[)
by Lm7,A30,A27,A29,XREAL_1:215;
for i be Nat st i in Seg n holds Da.i c= D.i
proof
let i be Nat;
assume
A35: i in Seg n; then
A36: Da.i = ].a.i-r0,a.i+r0.[ by A34;
D.i = ].a.i-r,a.i+r.[ by A33,A35;
hence thesis by A31,A27,A36,A32,INTEGRA6:2;
end; then
CarProduct Da c= CarProduct D by Th48; then
CarProduct Da c= A by A33;
hence thesis by A30,A34,A27,A29,XREAL_1:215;
end;
defpred Q[object,object] means
ex a be n-element FinSequence of REAL ,r be Real,
D be non-empty n-element FinSequence st
p.$1= PtCarProduct a & a is n-element FinSequence of RAT
& 0 < r & r = F.(PtCarProduct a) & $2 = CarProduct D
& (for i be Nat st i in Seg n holds D.i = ].a.i-r,a.i+r.[)
& CarProduct D c= A;
A37: for i being object st i in NAT
ex y being object st y in bool CarProduct X & Q[i,y]
proof
let i be object;
assume i in NAT; then
i in dom p by FUNCT_2:def 1; then
p.i in rng p by FUNCT_1:3; then
A38: p.i in A & p.i in CarProduct(Seg n --> RAT) by A25,XBOOLE_0:def 4; then
consider a be n-element FinSequence of RAT such that
A39: p.i = PtCarProduct a by Th46;
rng a c= REAL; then
reconsider a as n-element FinSequence of REAL by FINSEQ_1:def 4;
consider r be Real such that
A40: 0 < r & r = F.(PtCarProduct a)
& ex Da be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds Da.i = ].a.i-r,a.i+r.[)
& CarProduct Da c= A by A26,A38,A39;
consider Da be non-empty n-element FinSequence such that
A41: (for i be Nat st i in Seg n holds Da.i = ].a.i-r,a.i+r.[)
& CarProduct Da c= A by A40;
set E = CarProduct Da;
take y = E;
for i be Nat st i in Seg n holds Da.i c= X.i
proof
let i be Nat;
assume
A42: i in Seg n; then
A43: Da.i = ].a.i-r,a.i+r.[ by A41;
X.i = REAL by A42,FUNCOP_1:7;
hence thesis by A43;
end; then
CarProduct Da c= CarProduct X by Th48;
hence y in bool CarProduct X;
thus Q[i,y] by A39,A40,A41;
end;
consider B be Function of NAT,bool CarProduct X such that
A44: for i being object st i in NAT holds Q[i,B.i] from FUNCT_2:sch 1(A37);
reconsider B as SetSequence of CarProduct X;
now let z be object;
assume z in rng B; then
consider i be object such that
A45: i in dom B & z=B.i by FUNCT_1:def 3;
reconsider i as Nat by A45;
consider a be n-element FinSequence of REAL ,r be Real,
D be non-empty n-element FinSequence such that
A46: p.i = PtCarProduct a & a is n-element FinSequence of RAT
& 0 < r & r = F.(PtCarProduct a) & B.i = CarProduct D
& (for j be Nat st j in Seg n holds D.j = ].a.j-r,a.j+r.[)
& CarProduct D c= A by A44,ORDINAL1:def 12;
for j be Nat st j in Seg n holds D.j is Element of L-Field
proof
let j be Nat;
assume j in Seg n; then
D.j = ].a.j-r,a.j+r.[ by A46;
hence thesis by MEASUR10:5,MEASUR12:75;
end; then
CarProduct D is Element of Prod_Field(L-Field n) by Th39;
hence z in Prod_Field(L-Field n) by A45,A46;
end; then
rng B c= Prod_Field(L-Field n); then
reconsider B as SetSequence of Prod_Field(L-Field n) by RELAT_1:def 19;
now let z be object;
assume z in union rng B; then
consider Y being set such that
A47: z in Y & Y in rng B by TARSKI:def 4;
consider i be object such that
A48: i in dom B & Y =B.i by A47,FUNCT_1:def 3;
reconsider i as Nat by A48;
ex a be n-element FinSequence of REAL ,r be Real,
D be non-empty n-element FinSequence st
p.i = PtCarProduct a & a is n-element FinSequence of RAT
& 0 < r & r = F.(PtCarProduct a) & B.i = CarProduct D
& (for j be Nat st j in Seg n holds D.j = ].a.j-r,a.j+r.[)
& CarProduct D c= A by A44,ORDINAL1:def 12;
hence z in A by A47,A48;
end; then
A49: union rng B c= A;
now let z be object;
assume
A50: z in A; then
reconsider u=z as Point of CarProduct S;
consider e0 being Real such that
A51: e0 > 0 & Ball (u,e0) c= A by A50,A1,NDIFF_8:20;
reconsider e=e0/4 as Real;
A52: 0 < e & e < e0 by A51,XREAL_1:223,224; then
A53: Ball (u,e) c= Ball (u,e0) by NDIFF_8:15;
u in the carrier of CarProduct S; then
u in CarProduct X by Th42; then
consider xx be n-element FinSequence of REAL such that
A54: u = PtCarProduct xx by Th45;
reconsider d0 = (e/2)/n as Real;
reconsider dd=d0/2 as Real;
A55: 0 < e/2 & e/2 < e by A52,XREAL_1:215,216; then
A56: 0 < d0 & d0 <= (e/2)/1 by XREAL_1:139,118,NAT_1:14;
A57: 0 < (e/2)/2 & (e/2)/2 < e/2 by A55,XREAL_1:215,216;
A58: d0/2 = ((e/2)/2)/n by XCMPLX_1:48;
A59: 0 < d0/2 & d0/2 < d0 by A56,XREAL_1:215,216;
consider qxx be n-element FinSequence of RAT such that
A60: for i be Nat st i in Seg n holds qxx.i in ].xx.i-dd,xx.i+dd.[
by A56,Lm8,XREAL_1:215;
A61: for i be Nat st i in Seg n holds |.qxx.i-xx.i.| <= d0/2
proof
let i be Nat;
assume i in Seg n; then
qxx.i in ].xx.i-dd,xx.i+dd.[ by A60;
hence |.qxx.i-xx.i.| <= d0/2 by RCOMP_1:1;
end;
PtCarProduct qxx in CarProduct(Seg n --> RAT) by Th46; then
A62: PtCarProduct qxx in CarProduct X by Th49,TARSKI:def 3;
A63: PtCarProduct qxx in A
proof
reconsider v = PtCarProduct qxx as Point of CarProduct S by A62,Th42;
rng qxx c= REAL; then
qxx is n-element FinSequence of REAL by FINSEQ_1:def 4; then
||. v-u .|| <= (e/2)/2 by A58,A54,A61,A51,Lm11; then
||. u-v .|| <= (e/2)/2 by NORMSP_1:7; then
||. u-v .|| <= (e/2) by XXREAL_0:2,A57; then
||. u-v .|| < e by XXREAL_0:2,A55; then
v in Ball (u,e);
hence PtCarProduct qxx in A by A53,A51;
end;
PtCarProduct qxx in CarProduct(Seg n -->RAT) by Th46; then
PtCarProduct qxx in rng p by A25,A63,XBOOLE_0:def 4; then
consider k be object such that
A64: k in dom p & p.k = PtCarProduct qxx by FUNCT_1:def 3;
reconsider k as Nat by A64;
rng qxx c= REAL; then
qxx is n-element FinSequence of REAL by FINSEQ_1:def 4; then
consider Rx be real-membered set such that
A65: Rx is non empty bounded_above
& Rx = {r where r is Real :0 < r
& ex D be non-empty n-element FinSequence st
(for i be Nat st i in Seg n holds D.i = ].qxx.i-r,qxx.i+r.[)
& CarProduct D c= A}
& F.(PtCarProduct qxx) = (upper_bound Rx)/2 by A63,A15;
consider ak be n-element FinSequence of REAL, rk be Real,
Dk be non-empty n-element FinSequence such that
A66: p.k = PtCarProduct ak & ak is n-element FinSequence of RAT
& 0 < rk & rk = F.(PtCarProduct ak) & B.k = CarProduct Dk
& (for j be Nat st j in Seg n holds Dk.j = ].ak.j-rk,ak.j+rk.[)
& CarProduct Dk c= A by A44,ORDINAL1:def 12;
A67: ak = qxx by A64,A66,Th5;
consider D1 be non-empty n-element FinSequence such that
A68: for i be Nat st i in Seg n holds D1.i = ].ak.i-d0,ak.i+d0.[
by A55,Lm7,XREAL_1:139;
reconsider m = n-1 as Nat by NAT_1:14,21;
now let z be object;
assume
A69: z in CarProduct D1;
for i be Nat st i in Seg n holds D1.i c= X.i
proof
let i be Nat;
assume
A70: i in Seg n; then
A71: D1.i = ].ak.i-d0,ak.i+d0.[ by A68;
X.i =REAL by A70,FUNCOP_1:7;
hence thesis by A71;
end; then
A72: CarProduct D1 c= CarProduct X by Th48; then
consider pz be n-element FinSequence of REAL such that
A73: z = PtCarProduct pz by A69,Th45;
A74: for i be Nat st i in Seg n holds pz.i in ].ak.i-d0,ak.i+d0.[
proof
let i be Nat;
assume
A75: i in Seg n; then
pz.i in D1.i by A73,A69,Th33;
hence thesis by A75,A68;
end;
reconsider v = z as Point of CarProduct S by A69,A72,Th42;
now let i be Nat;
assume
A76: i in Seg n; then
pz.i in ].ak.i-d0,ak.i+d0.[ by A74; then
|. pz.i-ak.i .| < d0 by RCOMP_1:1; then
A77: |. ak.i-pz.i .| <d0 by COMPLEX1:60;
A78: |.xx.i-pz.i.| <=|.xx.i-ak.i.| + |.ak.i-pz.i.| by COMPLEX1:63;
|. ak.i-xx.i .| <= d0/2 by A76,A61,A67; then
|. ak.i-xx.i .| <= d0 by A59,XXREAL_0:2; then
|.xx.i-ak.i.| <=d0 by COMPLEX1:60; then
A79: |.xx.i-ak.i.| + |.ak.i-pz.i.| <= d0 + d0 by A77,XREAL_1:7;
d0+d0 = ( (e/2)+ (e/2) )/n by XCMPLX_1:62;
hence |.xx.i-pz.i.| <= e/n by A78,A79,XXREAL_0:2;
end; then
||. u-v .|| <= e by A54,A51,A73,Lm11; then
||. u-v .|| < e0 by A52,XXREAL_0:2; then
v in Ball(u,e0);
hence z in A by A51;
end; then
CarProduct D1 c= A; then
d0 in Rx by A65,A67,A56,A68; then
A80: d0 <= upper_bound Rx by A65,SEQ_4:def 1;
now let i be Nat;
assume
A81: i in Seg n; then
ak.i in ].xx.i-(d0/2),xx.i+(d0/2).[ by A67,A60; then
|.ak.i -xx.i .| < (d0/2) by RCOMP_1:1; then
A82: |.xx.i -ak.i .| < (d0/2) by COMPLEX1:60;
].ak.i-d0/2,ak.i+d0/2 .[ c= ].ak.i-rk,ak.i+rk.[
by A80,A65,A66,A64,XREAL_1:72,INTEGRA6:2; then
xx.i in ].ak.i-rk,ak.i+rk .[ by A82,RCOMP_1:1;
hence xx.i in Dk.i by A66,A81;
end; then
A83: u in B.k by A66,A54,Th61;
k in NAT by ORDINAL1:def 12; then
k in dom B by FUNCT_2:def 1; then
B.k in rng B by FUNCT_1:3;
hence z in union rng B by A83,TARSKI:def 4;
end; then
A c= union rng B; then
Union B = A by A49,CARD_3:def 4;
hence A in Prod_Field(L-Field n) by PROB_1:17;
end;
end;
end;
theorem
for n be non zero Nat,
f be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
g be PartFunc of CarProduct(Seg n --> REAL),REAL,
E be Element of Prod_Field(L-Field n)
st f = g & f is_continuous_on E & dom f = E holds g is E-measurable
proof
let n be non zero Nat,
f be PartFunc of CarProduct(Seg n --> RNS_Real),RNS_Real,
g be PartFunc of CarProduct(Seg n --> REAL),REAL,
E be Element of Prod_Field(L-Field n);
assume
A1: f = g & f is_continuous_on E & dom f = E;
for r being Real holds E /\ (less_dom (g,r)) in Prod_Field(L-Field n)
proof
let r be Real;
A2: less_dom(g,r) = g"( ].-infty,r.[ ) by Th63;
consider H be Subset of CarProduct(Seg n --> RNS_Real) such that
A3: H /\ E = f"( ].-infty,r.[ ) & H is open by Th62,A1;
H in Prod_Field(L-Field n) by A3,Th67; then
less_dom(g,r) in Prod_Field(L-Field n) by A1,A2,A3,FINSUB_1:def 2;
hence E /\ (less_dom (g,r)) in Prod_Field(L-Field n) by FINSUB_1:def 2;
end;
hence thesis by MESFUNC6:12;
end;
theorem Th69:
for n be non zero Nat, px be object holds
px is n-element FinSequence of REAL iff px in product(Seg n --> REAL)
proof
let n be non zero Nat, px be object;
thus px is n-element FinSequence of REAL implies
px in product(Seg n --> REAL) by Th43;
assume px in product(Seg n --> REAL); then
px in REAL n by SRINGS_5:8; then
px in n-tuples_on REAL by EUCLID:def 1;
hence px is n-element FinSequence of REAL by FINSEQ_2:131;
end;
theorem
for n be non zero Nat, x be object holds
x in CarProduct(Seg n--> REAL) iff
ex px be n-element FinSequence of REAL
st px in product(Seg n--> REAL) & x = PtCarProduct px
proof
let n be non zero Nat, x be object;
hereby assume x in CarProduct(Seg n-->REAL); then
consider px be n-element FinSequence of REAL such that
A1: x = PtCarProduct px by Th45;
take px;
thus px in product(Seg n-->REAL) & x = PtCarProduct px by A1,Th69;
end;
assume ex px be n-element FinSequence of REAL st
px in product(Seg n--> REAL) & x = PtCarProduct px;
hence x in CarProduct(Seg n--> REAL) by Th45;
end;
theorem Th71:
for n be non zero Nat holds carr(Seg n --> RNS_Real) = Seg n --> REAL
proof
let n be non zero Nat;
set J = Seg n --> RNS_Real;
set I = Seg n --> REAL;
A1: n is Element of NAT by ORDINAL1:def 12;
dom I = Seg n; then
A2: len I = n by FINSEQ_1:def 3,A1;
dom J = Seg n; then
A3: len J = n by FINSEQ_1:def 3,A1;
for j being Element of dom J holds I.j = the carrier of (J.j);
hence thesis by A2,A3,PRVECT_1:def 11;
end;
theorem Th72:
for n be non zero Nat holds
CarProd(Seg n --> RNS_Real) = CarProd(Seg n --> REAL)
proof
let n be non zero Nat;
set I = CarProd(Seg n --> RNS_Real);
ex CX be non-empty n-element FinSequence st
CX = carr (Seg n--> RNS_Real)
& CarProduct CX = the carrier of CarProduct(Seg n--> RNS_Real)
& I = CarProd CX & I is bijective by Def7;
hence thesis by Th71;
end;
theorem Th73:
for n be non zero Nat, D be non-empty n-element FinSequence st
for i be Nat st i in Seg n holds D.i c= REAL
holds product D = (CarProd(Seg n --> REAL)).:(CarProduct D)
proof
let n be non zero Nat, D be non-empty n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds D.i c= REAL;
set I = CarProd(Seg n --> RNS_Real);
A2: dom I = the carrier of CarProduct(Seg n --> RNS_Real) by FUNCT_2:def 1;
CarProduct D c= CarProduct(Seg n -->REAL) by A1,Th34; then
A3: CarProduct D c= the carrier of CarProduct(Seg n-->RNS_Real) by Th42;
for x be object holds x in product D iff x in I.:(CarProduct D)
proof
let x be object;
hereby assume
A4: x in product D; then
consider g being Function such that
A5: x = g & dom g = dom D
& for y being object st y in dom D holds g.y in D.y by CARD_3:def 5;
A6: dom D = Seg len D by FINSEQ_1:def 3; then
reconsider t=x as FinSequence by A5,FINSEQ_1:def 2;
dom D = Seg n by A6,CARD_1:def 7; then
Seg len t = Seg n by A5,FINSEQ_1:def 3; then
reconsider y = t as n-element FinSequence by FINSEQ_1:6,CARD_1:def 7;
A7: PtCarProduct y in CarProduct D by Th6,A4;
reconsider s = PtCarProduct y
as Point of CarProduct(Seg n-->RNS_Real) by A3,A4,Th6;
consider px be n-element FinSequence such that
A8: s = PtCarProduct px & I.s = px by Th28;
px = y by A8,Th5;
hence x in I.:(CarProduct D) by A2,A7,A8,FUNCT_1:def 6;
end;
assume x in I.:(CarProduct D); then
consider t being object such that
A9: t in dom I & t in CarProduct D & x = I.t by FUNCT_1:def 6;
reconsider s=t as Point of CarProduct(Seg n-->RNS_Real) by A9;
A10: ex px be n-element FinSequence st
s = PtCarProduct px & I.s = px by Th28;
ex qx be n-element FinSequence st
qx in product D & t = PtCarProduct qx by A9,Th6;
hence x in product D by A9,A10,Th5;
end; then
product D = I.:(CarProduct D) by TARSKI:2;
hence thesis by Th72;
end;
theorem Th74:
for n be non zero Nat holds
ex I be LinearOperator of
CarProduct(Seg n-->RNS_Real),product(Seg n-->RNS_Real)
st I = CarProd(Seg n-->RNS_Real) & I is one-to-one onto isometric
proof
let n be non zero Nat;
set I = CarProd(Seg n-->RNS_Real);
consider CX be non-empty n-element FinSequence such that
A1: CX = carr (Seg n--> RNS_Real)
& CarProduct CX = the carrier of CarProduct(Seg n--> RNS_Real)
& I = CarProd CX & I is bijective by Def7;
A2: for x,y be Element of CarProduct(Seg n--> RNS_Real) holds
I.(x+y) = (I.x) + (I.y) by Th29;
for x being VECTOR of CarProduct(Seg n-->RNS_Real ), r being Real holds
I.(r*x) = r*(I.x)
proof
let x be VECTOR of CarProduct(Seg n-->RNS_Real ), r be Real;
r in REAL by XREAL_0:def 1;
hence thesis by Th30;
end; then
reconsider I as LinearOperator of
CarProduct(Seg n-->RNS_Real),product(Seg n-->RNS_Real)
by A2,LOPBAN_1:def 5,VECTSP_1:def 20;
take I;
thus I = CarProd(Seg n-->RNS_Real);
for x being Element of CarProduct(Seg n-->RNS_Real) holds
||. I.x .|| = ||. x .|| by Th31;
hence I is one-to-one onto isometric by A1,NDIFF_7:7;
end;
theorem
for n be non zero Nat, s be sequence of CarProduct(Seg n-->RNS_Real) holds
s is convergent iff CarProd(Seg n-->RNS_Real)*s is convergent
proof
let n be non zero Nat, s be sequence of CarProduct(Seg n-->RNS_Real);
ex I be LinearOperator of
CarProduct(Seg n-->RNS_Real),product(Seg n-->RNS_Real) st
I = CarProd(Seg n-->RNS_Real) & I is one-to-one onto isometric by Th74;
hence thesis by NDIFF_7:11;
end;
theorem Th76:
for n be non zero Nat, X be Subset of CarProduct(Seg n-->RNS_Real),
Y be Subset of product(Seg n-->RNS_Real) st
Y = (CarProd(Seg n-->RNS_Real)).:X holds
( X is closed iff Y is closed ) &
( X is open iff Y is open ) &
( X is compact iff Y is compact )
proof
let n be non zero Nat, X be Subset of CarProduct(Seg n-->RNS_Real),
Y be Subset of product(Seg n-->RNS_Real);
assume
A1: Y = (CarProd(Seg n-->RNS_Real)).:X;
ex I be LinearOperator of
CarProduct(Seg n-->RNS_Real ),product(Seg n-->RNS_Real) st
I = CarProd(Seg n-->RNS_Real) & I is one-to-one onto isometric by Th74;
hence thesis by A1,NDIFF_7:12,13,14;
end;
theorem
for n be non zero Nat, Z be RealNormSpace,
y be Point of product(Seg n-->RNS_Real),
x be Point of CarProduct(Seg n-->RNS_Real),
f be 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
let n be non zero Nat, Z be RealNormSpace,
y be Point of product(Seg n-->RNS_Real),
x be Point of CarProduct(Seg n-->RNS_Real),
f be PartFunc of product(Seg n-->RNS_Real),Z;
assume that
A1: y = (CarProd(Seg n-->RNS_Real)).x and
A2: y in dom f;
ex I be LinearOperator of
CarProduct(Seg n-->RNS_Real),product(Seg n-->RNS_Real) st
I = CarProd(Seg n-->RNS_Real) & I is one-to-one onto isometric by Th74;
hence thesis by A1,A2,NDIFF_7:15;
end;
theorem
for n be non zero Nat, Z be RealNormSpace,
X be Subset of product(Seg n-->RNS_Real),
Y be Subset of CarProduct(Seg n-->RNS_Real),
f be 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
let n be non zero Nat, Z be RealNormSpace,
X be Subset of product(Seg n-->RNS_Real),
Y be Subset of CarProduct(Seg n-->RNS_Real),
f be PartFunc of product(Seg n-->RNS_Real),Z;
assume
A1: Y = (CarProd(Seg n-->RNS_Real))"X;
ex I be LinearOperator of
CarProduct(Seg n-->RNS_Real),product(Seg n-->RNS_Real) st
I = CarProd(Seg n-->RNS_Real) & I is one-to-one onto isometric by Th74;
hence thesis by A1,NDIFF_7:16;
end;
theorem
for n be non zero Nat, D be non-empty n-element FinSequence st
for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL
holds
ex E be Subset of product(Seg n-->RNS_Real)
st E = product D & E is compact
proof
let n be non zero Nat, D be non-empty n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds D.i is closed_interval Subset of REAL;
consider E0 be Subset of CarProduct(Seg n-->RNS_Real) such that
A2: E0 = CarProduct D & E0 is compact by A1,Th51;
reconsider E = (CarProd(Seg n-->RNS_Real)).:E0
as Subset of product(Seg n-->RNS_Real);
take E;
now let i be Nat;
assume i in Seg n; then
D.i is closed_interval Subset of REAL by A1;
hence D.i c= REAL;
end; then
product D = (CarProd(Seg n --> REAL)).:(CarProduct D) by Th73;
hence thesis by A2,Th72,Th76;
end;
theorem
for n be non zero Nat, D be non-empty n-element FinSequence st
for i be Nat st i in Seg n holds D.i is Element of L-Field holds
product D is Element of XL-Field n
proof
let n be non zero Nat, D be non-empty n-element FinSequence;
assume
A1: for i be Nat st i in Seg n holds D.i is Element of L-Field; then
A3: CarProduct D is Element of Prod_Field(L-Field n) by Th39;
for i be Nat st i in Seg n holds D.i c= REAL
proof
let i be Nat;
assume i in Seg n; then
D.i is Element of L-Field by A1;
hence D.i c= REAL;
end; then
A2: product D = (CarProd(Seg n --> REAL)).:(CarProduct D) by Th73;
CarProd(Seg n --> REAL) is bijective by MEASUR14:12; then
(CarProd(Seg n --> REAL)).:(CarProduct D)
in CopyField(CarProd(Seg n --> REAL),Prod_Field(L-Field n))
by A3,MEASUR14:18; then
(CarProd(Seg n --> REAL)).:(CarProduct D)
in XProd_Field(L-Field n) by MEASUR14:def 7;
hence thesis by A2,MEASUR14:def 11;
end;
theorem
for n be non zero Nat, Y be Subset of product(Seg n-->RNS_Real) st
Y is open holds Y in XL-Field n
proof
let n be non zero Nat, Y be Subset of product(Seg n-->RNS_Real);
assume
A1: Y is open;
consider I be LinearOperator of
CarProduct(Seg n-->RNS_Real ),product(Seg n-->RNS_Real) such that
A2: I = CarProd(Seg n-->RNS_Real) & I is one-to-one onto isometric by Th74;
A3: rng I = the carrier of product (Seg n-->RNS_Real) by A2,FUNCT_2:def 3;
reconsider X = I"Y as Subset of CarProduct(Seg n-->RNS_Real);
A4: (CarProd(Seg n-->RNS_Real)).:X = Y by A2,A3,FUNCT_1:77; then
X is open iff Y is open by Th76; then
A5: X in Prod_Field(L-Field n) by A1,Th67;
A6: CarProd(Seg n-->RNS_Real) = CarProd(Seg n-->REAL) by Th72;
CarProd(Seg n --> REAL) is bijective by MEASUR14:12; then
(CarProd(Seg n --> REAL)).:X
in CopyField(CarProd(Seg n --> REAL),Prod_Field(L-Field n))
by A5,MEASUR14:18; then
(CarProd(Seg n --> REAL)).:X
in XProd_Field(L-Field n) by MEASUR14:def 7;
hence thesis by A4,A6,MEASUR14:def 11;
end;
theorem Th82:
for X,Y be non empty set, S be SigmaField of X, T be Function of X,Y,
F being Set_Sequence of S st T is bijective holds
((.:T) |S)*F is Set_Sequence of CopyField(T,S)
proof
let X,Y be non empty set, S be SigmaField of X, T be Function of X,Y,
F be Set_Sequence of S;
assume
A1: T is bijective;
set H = (.:T) |S;
rng H = (.:T).:S by RELAT_1:115; then
A2: rng H = CopyField(T,S) by A1,MEASUR14:def 2;
dom H = S by FUNCT_2:def 1; then
reconsider H as Function of S,CopyField(T,S) by A2,FUNCT_2:1;
rng F c= S
proof let z be object;
assume z in rng F; then
consider t be object such that
A3: t in dom F & z = F.t by FUNCT_1:def 3;
reconsider t as Nat by A3;
F.t in S;
hence z in S by A3;
end; then
rng F c= dom H by FUNCT_2:def 1; then
dom (H*F) = dom F by RELAT_1:27; then
A4: dom (H*F) = NAT by FUNCT_2:def 1;
rng (H*F) c= CopyField(T,S); then
reconsider HF = H*F as Function of NAT,CopyField(T,S) by A4,FUNCT_2:2;
rng HF c= bool Y; then
reconsider HF as SetSequence of Y by FUNCT_2:6;
for n being Nat holds HF.n in CopyField(T,S)
proof
let n be Nat;
HF.n = H.(F.n) by A4,FUNCT_1:12,ORDINAL1:def 12;
hence HF.n in CopyField(T,S);
end;
hence thesis by MEASURE8:def 2;
end;
theorem Th83:
for X,Y be non empty set, T be Function of X,Y, S be SigmaField of X,
M be sigma_Measure of S st T is bijective & M is sigma_finite holds
CopyMeasure(T,M) is sigma_finite
proof
let X,Y be non empty set, T be Function of X,Y, S be SigmaField of X,
M be sigma_Measure of S;
assume
A1: T is bijective & M is sigma_finite; then
consider E being Set_Sequence of S such that
A2: (for n being Nat holds M.(E.n) < +infty) & Union E = X by MEASUR11:def 12;
set M1 = CopyMeasure(T,M);
set S1 = CopyField(T,S);
.:T is bijective by A1,MEASUR14:1; then
A3: .:T is one-to-one onto;
reconsider E1= ((.:T) |S)*E as Set_Sequence of S1 by A1,Th82;
A4: for n being Nat holds M1.(E1.n) < +infty
proof
let n be Nat;
A5: M.(E.n) < +infty by A2;
consider t be Element of S such that
A6: E1.n = T.:t & M1.(E1.n) = M.t by A1,MEASUR14:def 4;
n in NAT by ORDINAL1:def 12; then
n in dom E by FUNCT_2:def 1; then
E1.n = ((.:T) |S).(E.n) by FUNCT_1:13; then
A7: E1.n = (.:T).(E.n) by FUNCT_1:49;
A8: T.:t = (.:T).t by A1,MEASUR14:1;
t in bool X & E.n in bool X; then
t in dom (.:T) & E.n in dom (.:T) by FUNCT_2:def 1;
hence thesis by A3,A6,A7,A8,A5;
end;
for z be object holds z in Union E1 iff z in Y
proof
let z be object;
thus z in Union E1 implies z in Y;
assume z in Y; then
z in rng T by A1,FUNCT_2:def 3; then
consider t be object such that
A9: t in dom T & z=T.t by FUNCT_1:def 3;
t in X by A9; then
t in union rng E by A2,CARD_3:def 4; then
consider En being set such that
A10: t in En & En in rng E by TARSKI:def 4;
consider n be object such that
A11: n in dom E & En = E.n by A10,FUNCT_1:def 3;
A12: n in NAT by A11;
reconsider n as Nat by A11;
A13: z in T.:En by A9,A10,FUNCT_1:def 6;
T.:En = (.:T).(E.n) by A11,A1,MEASUR14:1; then
T.:En = ((.:T) |S).(E.n) by FUNCT_1:49; then
A14: T.:En = E1.n by A11,FUNCT_1:13;
set E1n = E1.n;
n in dom E1 by A12,FUNCT_2:def 1; then
E1n in rng E1 by FUNCT_1:3; then
z in union rng E1 by A13,A14,TARSKI:def 4;
hence z in Union E1 by CARD_3:def 4;
end;
hence thesis by A4,MEASUR11:def 12,TARSKI:2;
end;
theorem
for n be non zero Nat holds XL-Meas n is sigma_finite
proof
let n be non zero Nat;
A1: REAL n = product (Seg n--> REAL) by SRINGS_5:8;
A2: CopyField(CarProd(Seg n-->REAL),Prod_Field(L-Field n))
= XProd_Field(L-Field n) by MEASUR14:def 7;
A3: XProd_Field(L-Field n) = XL-Field n by MEASUR14:def 11;
CarProd(Seg n--> REAL) is bijective by MEASUR14:12; then
CopyMeasure(CarProd(Seg n-->REAL),Prod_Measure(L-Meas n))
is sigma_finite by Th83,Th36; then
XProd_Measure(L-Meas n) is sigma_finite by A2,MEASUR14:def 8;
hence XL-Meas n is sigma_finite by A1,A3,MEASUR14:def 12;
end;
theorem Th85:
for n be non zero Nat, D be non-empty n-element FinSequence st
rng D c= L-Field holds CarProduct D in Prod_Field(L-Field n)
proof
defpred Q[non zero Nat] means
for D be non-empty $1-element FinSequence st
rng D c= L-Field holds CarProduct D in Prod_Field(L-Field $1);
A1: Q[1]
proof
let D be non-empty 1-element FinSequence;
assume
A2: rng D c= L-Field;
A3: CarProduct D = D.1 by MEASUR13:def 3;
A4: 1 in Seg 1;
len D = 1 by FINSEQ_3:153; then
1 in dom D by A4,FINSEQ_1:def 3;
hence CarProduct D in Prod_Field(L-Field 1)
by A2,A3,FUNCT_1:3,MEASUR14:41;
end;
A5: for n be non zero Nat st Q[n] holds Q[n+1]
proof
let n be non zero Nat;
assume
A6: Q[n];
let D be non-empty (n+1)-element FinSequence;
assume
A7: rng D c= L-Field;
A8: CarProduct D = [: CarProduct SubFin(D,n),ElmFin(D,n+1) :] by MEASUR13:6;
set D1 = SubFin(D,n);
n < n+1 by NAT_1:13; then
SubFin(D,n) = D|n by MEASUR13:def 5; then
rng D1 c= rng D by RELAT_1:70; then
rng D1 c= L-Field by A7; then
A9: CarProduct D1 in Prod_Field(L-Field n) by A6;
A10: len D = n+1 by FINSEQ_3:153;
n+1 in Seg(n+1) by FINSEQ_1:3; then
A11: n+1 in dom D by A10,FINSEQ_1:def 3;
ElmFin(D,n+1) = D.(n+1) by MEASUR13:def 1; then
ElmFin(D,n+1) in rng D by A11,FUNCT_1:3; then
A12: CarProduct D in measurable_rectangles(Prod_Field(L-Field n),L-Field)
by A7,A8,A9;
measurable_rectangles(Prod_Field(L-Field n),L-Field)
c= sigma measurable_rectangles(Prod_Field(L-Field n),L-Field)
by PROB_1:def 9; then
CarProduct D
in sigma measurable_rectangles(Prod_Field(L-Field n),L-Field) by A12;
hence CarProduct D in Prod_Field(L-Field(n+1)) by MEASUR14:44;
end;
A13: for n be non zero Nat holds Q[n] from NAT_1:sch 10(A1,A5);
let n be non zero Nat, D be non-empty n-element FinSequence;
assume rng D c= L-Field;
hence thesis by A13;
end;
theorem Th86:
for n be non zero Nat, D be non-empty n-element FinSequence st
rng D c= L-Field &
(for i be Nat st i in Seg n holds L-Meas.(D.i) in REAL)
holds ex E be n-element FinSequence of REAL
st ( for i be Nat st i in Seg n holds E.i = L-Meas.(D.i) )
& (Prod_Measure(L-Meas n)).(CarProduct D) = Product E
proof
defpred Q[non zero Nat] means
for D be non-empty $1-element FinSequence
st rng D c= L-Field
& (for i be Nat st i in Seg $1 holds L-Meas.(D.i) in REAL) holds
ex E be $1-element FinSequence of REAL
st ( for i be Nat st i in Seg $1 holds E.i = L-Meas.(D.i) )
& (Prod_Measure(L-Meas $1)).(CarProduct D) = Product E;
A1: Q[1]
proof
let D be non-empty 1-element FinSequence;
assume
A2: rng D c= L-Field
& for i be Nat st i in Seg 1 holds L-Meas.(D.i) in REAL;
A3: CarProduct D = D.1 by MEASUR13:def 3;
len D = 1 by FINSEQ_3:153; then
1 in dom D by FINSEQ_3:25; then
reconsider D1=D.1 as Element of L-Field by A2,FUNCT_1:3;
set E = <*L-Meas.D1*>;
1 in Seg 1; then
A4: L-Meas.D1 in REAL by A2; then
reconsider E as 1-element FinSequence of REAL by FINSEQ_1:74;
take E;
now let i be Nat;
assume
A5: i in Seg 1; then
E.i = E.1 by FINSEQ_1:2,TARSKI:def 1;
hence E.i = L-Meas.(D.i) by A5,FINSEQ_1:2,TARSKI:def 1;
end;
hence thesis by A4,A3,MEASUR14:45,RVSUM_1:95;
end;
A6: for n be non zero Nat st Q[n] holds Q[n+1]
proof
let n be non zero Nat;
assume
A7: Q[n];
let D be non-empty (n+1)-element FinSequence;
assume
A8: rng D c= L-Field
& for i be Nat st i in Seg (n+1) holds L-Meas.(D.i) in REAL;
A11: Seg n c= Seg (n+1) by NAT_1:12,FINSEQ_1:5;
A9: CarProduct D = [: CarProduct SubFin(D,n),ElmFin(D,n+1) :]
by MEASUR13:6;
n < n+1 by NAT_1:13; then
A10: SubFin(D,n) = D|n & ElmFin(D,n+1) = D.(n+1) by MEASUR13:def 1,def 5;
then rng SubFin(D,n) c= rng D by RELAT_1:70; then
A12: rng SubFin(D,n) c= L-Field by A8;
now let i be Nat;
assume
A13: i in Seg n; then
SubFin(D,n).i = D.i by A10,FUNCT_1:49;
hence L-Meas.(SubFin(D,n).i) in REAL by A8,A11,A13;
end; then
consider En be n-element FinSequence of REAL such that
A14: ( for i be Nat st i in Seg n holds En.i = L-Meas.(SubFin(D,n).i) )
& (Prod_Measure(L-Meas n)).CarProduct(SubFin(D,n)) = Product En by A12,A7;
set E = En ^ <*L-Meas.(D.(n+1))*>;
A15: n+1 in Seg (n+1) by FINSEQ_1:3;
len D = n+1 by FINSEQ_3:153; then
n+1 in dom D by A15,FINSEQ_1:def 3; then
reconsider Dn1 = D.(n+1) as Element of L-Field by A8,FUNCT_1:3;
set En1 = <*L-Meas.Dn1*>;
A16: rng En1 = {L-Meas.Dn1} by FINSEQ_1:38;
A17: L-Meas.Dn1 in REAL by A8,FINSEQ_1:3; then
reconsider En1 as 1-element FinSequence of REAL
by A16,ZFMISC_1:31,FINSEQ_1:def 4;
rng (En ^ En1) c= REAL; then
reconsider E as FinSequence of REAL;
A18: len En = n by CARD_1:def 7;
reconsider E as (n+1)-element FinSequence of REAL;
take E;
thus for i be Nat st i in Seg (n+1) holds E.i = L-Meas.(D.i)
proof
let i be Nat;
assume i in Seg (n+1); then
A19: 1 <= i & i <= n+1 by FINSEQ_1:1;
now assume i <> n+1; then
i < n+1 by A19,XXREAL_0:1; then
i <= n by NAT_1:13; then
A20: i in Seg n by A19; then
i in dom En by FINSEQ_1:def 3,A18; then
E.i = En.i by FINSEQ_1:def 7; then
E.i = L-Meas.(SubFin(D,n).i) by A14,A20;
hence E.i = L-Meas.(D.i) by A10,A20,FUNCT_1:49;
end;
hence thesis by A18,FINSEQ_1:42;
end;
A21: Prod_Measure L-Meas(n+1)
= Prod_Measure(Prod_Measure L-Meas n,L-Meas) by MEASUR14:48;
reconsider Y = Seg (n+1)--> REAL as (n+1)-element FinSequence;
reconsider sEn = En as real-valued FinSequence;
reconsider sLn1 = L-Meas.Dn1 as Real by A17;
Product E = (Product sEn) * sLn1 by RVSUM_1:96; then
A22: Product E = (Product En) * (L-Meas.Dn1) by EXTREAL1:1;
A23: CarProduct(SubFin(D,n)) in Prod_Field L-Field n by A12,Th85; then
A24: [: CarProduct SubFin(D,n),Dn1 :] in
measurable_rectangles(Prod_Field L-Field n,L-Field);
measurable_rectangles(Prod_Field L-Field n,L-Field)
c= sigma measurable_rectangles(Prod_Field L-Field n,L-Field)
by PROB_1:def 9; then
reconsider H = [:CarProduct SubFin(D,n),Dn1:]
as Element of sigma measurable_rectangles
(Prod_Field L-Field n,L-Field) by A24;
(product_sigma_Measure(Prod_Measure L-Meas n,L-Meas)).H
= ((Prod_Measure L-Meas n).CarProduct(SubFin(D,n))) * L-Meas.Dn1
by A23,MEASUR11:16;
hence thesis by A14,A22,A10,A21,A9,MESFUN12:def 9;
end;
A25:for n be non zero Nat holds Q[n] from NAT_1:sch 10(A1,A6);
let n be non zero Nat, E be non-empty n-element FinSequence;
assume rng E c= L-Field
& for i be Nat st i in Seg n holds L-Meas.(E.i) in REAL;
hence thesis by A25;
end;
theorem
for n be non zero Nat, D be non-empty n-element FinSequence st
rng D c= L-Field &
for i be Nat st i in Seg n holds L-Meas.(D.i) in REAL holds
ex E be n-element FinSequence of REAL
st ( for i be Nat st i in Seg n holds E.i = L-Meas.(D.i) )
& (XL-Meas n).(product D) = Product E
proof
let n be non zero Nat, D be non-empty n-element FinSequence;
assume
A1: rng D c= L-Field
& for i be Nat st i in Seg n holds L-Meas.(D.i) in REAL;
A2: for i be Nat st i in Seg n holds D.i c= REAL
proof
let i be Nat;
assume i in Seg n; then
i in dom D by FINSEQ_1:89; then
D.i in L-Field by A1,FUNCT_1:3;
hence D.i c= REAL;
end; then
A3: product D = (CarProd(Seg n --> REAL)).:(CarProduct D) by Th73;
consider E be n-element FinSequence of REAL such that
A4: ( for i be Nat st i in Seg n holds E.i = L-Meas.(D.i))
& (Prod_Measure(L-Meas n)).(CarProduct D) = Product E by A1,Th86;
take E;
thus for i be Nat st i in Seg n holds E.i = L-Meas.(D.i) by A4;
set M = Prod_Measure(L-Meas n);
set S = Prod_Field(L-Field n);
set f = CarProd(Seg n --> REAL);
set M1 = CopyMeasure(f,M);
set S1 = CopyField(f,S);
A5: f is bijective by MEASUR14:12; then
.:f is bijective by MEASUR14:1; then
A6: .:f is one-to-one onto;
set H = (.:f) |S;
rng H = (.:f).:S by RELAT_1:115; then
A7:rng H = CopyField(f,S) by MEASUR14:def 2,12;
dom H = S by FUNCT_2:def 1; then
reconsider H as Function of S,CopyField(f,S) by A7,FUNCT_2:1;
CarProduct D c= CarProduct(Seg n --> REAL) by A2,Th34; then
A8:product D = (.:f).(CarProduct D) by A5,A3,MEASUR14:1;
for i be Nat st i in Seg n holds D.i is Element of L-Field
proof
let i be Nat;
assume i in Seg n; then
i in dom D by FINSEQ_1:89; then
D.i in rng D by FUNCT_1:def 3;
hence D.i is Element of L-Field by A1;
end; then
A9:CarProduct D is Element of Prod_Field(L-Field n) by Th39; then
product D = H.(CarProduct D) by FUNCT_1:49,A8; then
product D in CopyField(f,S) by A9,FUNCT_2:5; then
consider t be Element of S such that
A10:product D = f.:t & M1.(product D) = M.t by A5,MEASUR14:def 4;
A11:f.:t = (.:f).t by A5,MEASUR14:1;
XL-Meas n = XProd_Measure(L-Meas n) by MEASUR14:def 12; then
A12: XL-Meas n = CopyMeasure(CarProd(Seg n-->REAL),Prod_Measure(L-Meas n))
by MEASUR14:def 8;
t in bool CarProduct(Seg n --> REAL)
& CarProduct D in bool CarProduct(Seg n --> REAL) by A9; then
t in dom (.:f) & CarProduct D in dom (.:f) by FUNCT_2:def 1;
hence thesis by A4,A6,A10,A11,A8,A12;
end;