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

proof

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;

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
{} 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

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;

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
Intersection A1 in { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y }

proof

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₁[ 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₁[n,Bn]

proof

let n be Element of NAT ; :: thesis: ex Bn being Element of bool Omega2 st S₁[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₁[n,Bn] by A10; :: thesis: verum

end;

consider B being Function of NAT,(bool Omega2) such that
A11: for x being Element of NAT holds S₁[x,B . x] from FUNCT_2:sch 3(A9);
reconsider B = B as SetSequence of bool Omega2 ;

now :: thesis: for y being object st y in rng B holds
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;

then rng B c= S2 ;
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;

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