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

for y being Element of S2 st y <> {} holds

{ z where z is Element of Omega1 : F . z is Element of y } = F " y

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

for F being random_variable of S1,S2

for y being Element of S2 st y <> {} holds

{ z where z is Element of Omega1 : F . z is Element of y } = F " y

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

for y being Element of S2 st y <> {} holds

{ z where z is Element of Omega1 : F . z is Element of y } = F " y

let F be random_variable of S1,S2; :: thesis: for y being Element of S2 st y <> {} holds

{ z where z is Element of Omega1 : F . z is Element of y } = F " y

let y be Element of S2; :: thesis: ( y <> {} implies { z where z is Element of Omega1 : F . z is Element of y } = F " y )

assume A1: y <> {} ; :: thesis: { z where z is Element of Omega1 : F . z is Element of y } = F " y

set D = { z where z is Element of Omega1 : F . z is Element of y } ;

for x being object holds

( x in { z where z is Element of Omega1 : F . z is Element of y } iff x in F " y )

for S2 being SigmaField of Omega2

for F being random_variable of S1,S2

for y being Element of S2 st y <> {} holds

{ z where z is Element of Omega1 : F . z is Element of y } = F " y

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

for F being random_variable of S1,S2

for y being Element of S2 st y <> {} holds

{ z where z is Element of Omega1 : F . z is Element of y } = F " y

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

for y being Element of S2 st y <> {} holds

{ z where z is Element of Omega1 : F . z is Element of y } = F " y

let F be random_variable of S1,S2; :: thesis: for y being Element of S2 st y <> {} holds

{ z where z is Element of Omega1 : F . z is Element of y } = F " y

let y be Element of S2; :: thesis: ( y <> {} implies { z where z is Element of Omega1 : F . z is Element of y } = F " y )

assume A1: y <> {} ; :: thesis: { z where z is Element of Omega1 : F . z is Element of y } = F " y

set D = { z where z is Element of Omega1 : F . z is Element of y } ;

for x being object holds

( x in { z where z is Element of Omega1 : F . z is Element of y } iff x in F " y )

proof

hence
{ z where z is Element of Omega1 : F . z is Element of y } = F " y
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in { z where z is Element of Omega1 : F . z is Element of y } iff x in F " y )

then ( x in dom F & F . x in y ) by FUNCT_1:def 7;

hence x in { z where z is Element of Omega1 : F . z is Element of y } ; :: thesis: verum

end;hereby :: thesis: ( x in F " y implies x in { z where z is Element of Omega1 : F . z is Element of y } )

assume
x in F " y
; :: thesis: x in { z where z is Element of Omega1 : F . z is Element of y } assume
x in { z where z is Element of Omega1 : F . z is Element of y }
; :: thesis: x in F " y

then consider z being Element of Omega1 such that

A2: ( x = z & F . z is Element of y ) ;

z in Omega1 ;

then z in dom F by FUNCT_2:def 1;

hence x in F " y by A2, FUNCT_1:def 7, A1; :: thesis: verum

end;then consider z being Element of Omega1 such that

A2: ( x = z & F . z is Element of y ) ;

z in Omega1 ;

then z in dom F by FUNCT_2:def 1;

hence x in F " y by A2, FUNCT_1:def 7, A1; :: thesis: verum

then ( x in dom F & F . x in y ) by FUNCT_1:def 7;

hence x in { z where z is Element of Omega1 : F . z is Element of y } ; :: thesis: verum