let k1 be Element of REAL ; for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega
for I being non empty real-membered set
for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let Omega be non empty set ; ( Omega = {1,2,3,4} implies for Sigma being SigmaField of Omega
for I being non empty real-membered set
for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like ) )
assume A0:
Omega = {1,2,3,4}
; for Sigma being SigmaField of Omega
for I being non empty real-membered set
for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let Sigma be SigmaField of Omega; for I being non empty real-membered set
for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let I be non empty real-membered set ; for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let MyFunc be ManySortedSigmaField of I,Sigma; ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} implies for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like ) )
assume A2:
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} )
; for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let eli be Element of I; ( eli = 1 implies ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like ) )
assume A4:
eli = 1
; ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
consider f being Function of Omega,REAL such that
A3:
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 )
by A0, MYF30;
take
f
; ( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
set i = eli;
for x being set holds f " x in El_Filtration (eli,MyFunc)
proof
let x be
set ;
f " x in El_Filtration (eli,MyFunc)
f " x in MyFunc . eli
proof
f " x in {{},{1,2,3,4}}
proof
(
f " x = {} or
f " x = {1,2,3,4} )
proof
per cases
( k1 in x or not k1 in x )
;
suppose JSUPP1:
k1 in x
;
( f " x = {} or f " x = {1,2,3,4} )
for
z being
object holds
(
z in {1,2,3,4} iff ex
y being
object st
(
[z,y] in f &
y in x ) )
proof
let z be
object ;
( z in {1,2,3,4} iff ex y being object st
( [z,y] in f & y in x ) )
I1:
(
z in {1,2,3,4} implies ex
y being
object st
(
[z,y] in f &
y in x ) )
( ex
y being
object st
(
[z,y] in f &
y in x ) implies
z in {1,2,3,4} )
hence
(
z in {1,2,3,4} iff ex
y being
object st
(
[z,y] in f &
y in x ) )
by I1;
verum
end; hence
(
f " x = {} or
f " x = {1,2,3,4} )
by RELAT_1:def 14;
verum end; end;
end;
hence
f " x in {{},{1,2,3,4}}
by TARSKI:def 2;
verum
end;
hence
f " x in MyFunc . eli
by A4, A2;
verum
end;
hence
f " x in El_Filtration (
eli,
MyFunc)
;
verum
end;
hence
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
by A3; verum