let Omega1, Omega2 be non empty set ; :: thesis: for S1 being SigmaField of Omega1

for S2 being SigmaField of Omega2

for F being random_variable of S1,S2 holds

( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )

let S1 be SigmaField of Omega1; :: thesis: for S2 being SigmaField of Omega2

for F being random_variable of S1,S2 holds

( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )

let S2 be SigmaField of Omega2; :: thesis: for F being random_variable of S1,S2 holds

( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )

let F be random_variable of S1,S2; :: thesis: ( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )

set S = { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ;

for x being object st x in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } holds

x in S1

{} is Element of S2 by PROB_1:22;

then A3: F " {} in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ;

A4: for A being Subset of Omega1 st A in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } holds

A ` in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y }

Intersection A1 in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y }

for S2 being SigmaField of Omega2

for F being random_variable of S1,S2 holds

( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )

let S1 be SigmaField of Omega1; :: thesis: for S2 being SigmaField of Omega2

for F being random_variable of S1,S2 holds

( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )

let S2 be SigmaField of Omega2; :: thesis: for F being random_variable of S1,S2 holds

( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )

let F be random_variable of S1,S2; :: thesis: ( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )

set S = { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ;

for x being object st x in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } holds

x in S1

proof

hence A2:
{ x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1
; :: thesis: { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1
let z be object ; :: thesis: ( z in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } implies z in S1 )

assume z in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ; :: thesis: z in S1

then consider x being Subset of Omega1 such that

A1: ( z = x & ex y being Element of S2 st x = F " y ) ;

thus z in S1 by A1, FINANCE1:def 5; :: thesis: verum

end;assume z in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ; :: thesis: z in S1

then consider x being Subset of Omega1 such that

A1: ( z = x & ex y being Element of S2 st x = F " y ) ;

thus z in S1 by A1, FINANCE1:def 5; :: thesis: verum

{} is Element of S2 by PROB_1:22;

then A3: F " {} in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ;

A4: for A being Subset of Omega1 st A in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } holds

A ` in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y }

proof

for A1 being SetSequence of Omega1 st rng A1 c= { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } holds
let A be Subset of Omega1; :: thesis: ( A in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } implies A ` in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } )

assume A in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ; :: thesis: A ` in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y }

then consider x being Subset of Omega1 such that

A5: ( A = x & ex y being Element of S2 st x = F " y ) ;

consider y being Element of S2 such that

A6: x = F " y by A5;

A7: y ` in S2 by PROB_1:def 1;

F " (y `) = (F " Omega2) \ (F " y) by FUNCT_1:69

.= A ` by A5, A6, FUNCT_2:40 ;

hence A ` in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } by A7; :: thesis: verum

end;assume A in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ; :: thesis: A ` in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y }

then consider x being Subset of Omega1 such that

A5: ( A = x & ex y being Element of S2 st x = F " y ) ;

consider y being Element of S2 such that

A6: x = F " y by A5;

A7: y ` in S2 by PROB_1:def 1;

F " (y `) = (F " Omega2) \ (F " y) by FUNCT_1:69

.= A ` by A5, A6, FUNCT_2:40 ;

hence A ` in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } by A7; :: thesis: verum

Intersection A1 in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y }

proof

hence
{ x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1
by PROB_1:15, A3, A4, A2, XBOOLE_1:1; :: thesis: verum
let A1 be SetSequence of Omega1; :: thesis: ( rng A1 c= { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } implies Intersection A1 in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } )

assume A8: rng A1 c= { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ; :: thesis: Intersection A1 in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y }

defpred S_{1}[ set , set ] means ( A1 . $1 = F " $2 & $2 in S2 );

A9: for n being Element of NAT ex Bn being Element of bool Omega2 st S_{1}[n,Bn]

A11: for x being Element of NAT holds S_{1}[x,B . x]
from FUNCT_2:sch 3(A9);

reconsider B = B as SetSequence of bool Omega2 ;

then reconsider B1 = Intersection B as Element of S2 by PROB_1:15;

F " B1 = Intersection A1 by Th3, A11;

hence Intersection A1 in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ; :: thesis: verum

end;assume A8: rng A1 c= { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ; :: thesis: Intersection A1 in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y }

defpred S

A9: for n being Element of NAT ex Bn being Element of bool Omega2 st S

proof

consider B being Function of NAT,(bool Omega2) such that
let n be Element of NAT ; :: thesis: ex Bn being Element of bool Omega2 st S_{1}[n,Bn]

A1 . n in rng A1 by FUNCT_2:112;

then A1 . n in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } by A8;

then consider x being Subset of Omega1 such that

A10: ( A1 . n = x & ex y being Element of S2 st x = F " y ) ;

thus ex Bn being Element of bool Omega2 st S_{1}[n,Bn]
by A10; :: thesis: verum

end;A1 . n in rng A1 by FUNCT_2:112;

then A1 . n in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } by A8;

then consider x being Subset of Omega1 such that

A10: ( A1 . n = x & ex y being Element of S2 st x = F " y ) ;

thus ex Bn being Element of bool Omega2 st S

A11: for x being Element of NAT holds S

reconsider B = B as SetSequence of bool Omega2 ;

now :: thesis: for y being object st y in rng B holds

y in S2

then
rng B c= S2
;y in S2

let y be object ; :: thesis: ( y in rng B implies y in S2 )

assume y in rng B ; :: thesis: y in S2

then consider x being object such that

A12: ( x in NAT & B . x = y ) by FUNCT_2:11;

reconsider x = x as Element of NAT by A12;

thus y in S2 by A12, A11; :: thesis: verum

end;assume y in rng B ; :: thesis: y in S2

then consider x being object such that

A12: ( x in NAT & B . x = y ) by FUNCT_2:11;

reconsider x = x as Element of NAT by A12;

thus y in S2 by A12, A11; :: thesis: verum

then reconsider B1 = Intersection B as Element of S2 by PROB_1:15;

F " B1 = Intersection A1 by Th3, A11;

hence Intersection A1 in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } ; :: thesis: verum