defpred S1[ Nat, set , set ] means ( ex i being non zero Nat st
( i = $1 & $2 is SigmaField of (CarProduct (SubFin (X,i))) ) implies ex i being non zero Nat ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( i = $1 & $2 = Si & $3 = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) );
A1:
for n being Nat st 1 <= n & n < m holds
for x being set ex y being set st S1[n,x,y]
proof
let n be
Nat;
( 1 <= n & n < m implies for x being set ex y being set st S1[n,x,y] )
assume
( 1
<= n &
n < m )
;
for x being set ex y being set st S1[n,x,y]
let x be
set ;
ex y being set st S1[n,x,y]
now ( ex k being non zero Nat st
( k = n & x is SigmaField of (CarProduct (SubFin (X,k))) ) implies ex y being set st S1[n,x,y] )assume
ex
k being non
zero Nat st
(
k = n &
x is
SigmaField of
(CarProduct (SubFin (X,k))) )
;
ex y being set st S1[n,x,y]then consider k being non
zero Nat such that A2:
(
k = n &
x is
SigmaField of
(CarProduct (SubFin (X,k))) )
;
reconsider Sn =
x as
SigmaField of
(CarProduct (SubFin (X,k))) by A2;
reconsider y =
sigma (measurable_rectangles (Sn,(ElmFin (S,(n + 1))))) as
set ;
take y =
y;
S1[n,x,y]thus
S1[
n,
x,
y]
by A2;
verum end;
hence
ex
y being
set st
S1[
n,
x,
y]
;
verum
end;
consider P being FinSequence such that
A3:
( len P = m & ( P . 1 = S . 1 or m = 0 ) & ( for n being Nat st 1 <= n & n < m holds
S1[n,P . n,P . (n + 1)] ) )
from RECDEF_1:sch 3(A1);
reconsider P = P as m -element FinSequence by A3, CARD_1:def 7;
defpred S2[ Nat] means ( 1 <= $1 & $1 <= m implies ex k being non zero Nat st
( k = $1 & P . $1 is SigmaField of (CarProduct (SubFin (X,k))) ) );
A4:
S2[ 0 ]
;
A5:
for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be
Nat;
( S2[n] implies S2[n + 1] )
assume A6:
S2[
n]
;
S2[n + 1]
assume A7:
( 1
<= n + 1 &
n + 1
<= m )
;
ex k being non zero Nat st
( k = n + 1 & P . (n + 1) is SigmaField of (CarProduct (SubFin (X,k))) )
per cases
( n = 0 or n <> 0 )
;
suppose A8:
n = 0
;
ex k being non zero Nat st
( k = n + 1 & P . (n + 1) is SigmaField of (CarProduct (SubFin (X,k))) )
1
<= m
by NAT_1:14;
then A9:
1
in Seg m
;
A10:
1
in Seg 1
;
reconsider k = 1 as non
zero Nat ;
take
k
;
( k = n + 1 & P . (n + 1) is SigmaField of (CarProduct (SubFin (X,k))) )thus
k = n + 1
by A8;
P . (n + 1) is SigmaField of (CarProduct (SubFin (X,k)))
SubFin (
X,
k)
= X | 1
by Def5, NAT_1:14;
then
CarProduct (SubFin (X,k)) = (X | k) . k
by Def3;
then
X . 1
= CarProduct (SubFin (X,k))
by A10, FUNCT_1:49;
hence
P . (n + 1) is
SigmaField of
(CarProduct (SubFin (X,k)))
by A3, A8, A9, Def2;
verum suppose A11:
n <> 0
;
ex k being non zero Nat st
( k = n + 1 & P . (n + 1) is SigmaField of (CarProduct (SubFin (X,k))) )then reconsider n1 =
n as non
zero Nat ;
A12:
( 1
<= n &
n < m )
by A11, A7, NAT_1:13, NAT_1:14;
then consider k being non
zero Nat,
Pk being
SigmaField of
(CarProduct (SubFin (X,k))) such that A13:
(
k = n &
P . n = Pk &
P . (n + 1) = sigma (measurable_rectangles (Pk,(ElmFin (S,(k + 1))))) )
by A3, A6;
CarProduct (SubFin (X,(k + 1))) = [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):]
by A12, A13, Th9;
hence
ex
k being non
zero Nat st
(
k = n + 1 &
P . (n + 1) is
SigmaField of
(CarProduct (SubFin (X,k))) )
by A13;
verum end;
end;
A14:
for n being Nat holds S2[n]
from NAT_1:sch 2(A4, A5);
for i being Nat st i in Seg m holds
P . i is SigmaField of ((ProdFinSeq X) . i)
proof
let i be
Nat;
( i in Seg m implies P . i is SigmaField of ((ProdFinSeq X) . i) )
assume A15:
i in Seg m
;
P . i is SigmaField of ((ProdFinSeq X) . i)
then A16:
( 1
<= i &
i <= m )
by FINSEQ_1:1;
per cases
( i = 1 or i <> 1 )
;
suppose
i <> 1
;
P . i is SigmaField of ((ProdFinSeq X) . i)then
1
< i
by A16, XXREAL_0:1;
then reconsider i1 =
i - 1 as non
zero Nat by NAT_1:20;
A18:
1
<= i1
by NAT_1:14;
i < m + 1
by A16, NAT_1:13;
then A19:
i1 < (m + 1) - 1
by XREAL_1:9;
then
S1[
i1,
P . i1,
P . (i1 + 1)]
by A3, A18;
then consider i2 being non
zero Nat,
Si being
SigmaField of
(CarProduct (SubFin (X,i2))) such that A20:
(
i2 = i1 &
P . i1 = Si &
P . (i1 + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i2 + 1))))) )
by A18, A19, A14;
A21:
(
i1 < i1 + 1 &
i1 + 1
<= m )
by A15, NAT_1:13, FINSEQ_1:1;
then
(
SubFin (
X,
i1)
= SubFin (
(SubFin (X,(i1 + 1))),
i1) &
ElmFin (
X,
(i1 + 1))
= ElmFin (
(SubFin (X,(i1 + 1))),
(i1 + 1)) )
by Th7, Th8;
then
[:(CarProduct (SubFin (X,i1))),(ElmFin (X,(i1 + 1))):] = (ProdFinSeq (SubFin (X,(i1 + 1)))) . (i1 + 1)
by A21, Th5;
then
[:(CarProduct (SubFin (X,i1))),(ElmFin (X,(i1 + 1))):] = (ProdFinSeq X) . (i1 + 1)
by A21, Th4;
hence
P . i is
SigmaField of
((ProdFinSeq X) . i)
by A20;
verum end;
end;
then reconsider P = P as sigmaFieldFamily of ProdFinSeq X by Def2;
take
P
; ( P . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = P . i & P . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) )
thus
P . 1 = S . 1
by A3; for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = P . i & P . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) )
thus
for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = P . i & P . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) )
verumproof
let i be non
zero Nat;
( i < m implies ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = P . i & P . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) )
assume A22:
i < m
;
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = P . i & P . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) )
A23:
1
<= i
by NAT_1:14;
then
S1[
i,
P . i,
P . (i + 1)]
by A3, A22;
hence
ex
Si being
SigmaField of
(CarProduct (SubFin (X,i))) st
(
Si = P . i &
P . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) )
by A14, A22, A23;
verum
end;