let k1, k2, k3, k4 be Element of REAL ; :: thesis: 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 = 3 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let Omega be non empty set ; :: thesis: ( 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 = 3 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like ) )
assume A0: Omega = {1,2,3,4} ; :: thesis: 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 = 3 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let Sigma be SigmaField of Omega; :: thesis: 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 = 3 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let I be non empty real-membered set ; :: thesis: 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 = 3 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let MyFunc be ManySortedSigmaField of I,Sigma; :: thesis: ( 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 = 3 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & 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} ) ; :: thesis: for eli being Element of I st eli = 3 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )
let eli be Element of I; :: thesis: ( eli = 3 implies ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like ) )
assume A4: eli = 3 ; :: thesis: ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & 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 = k2 & f . 3 = k3 & f . 4 = k4 ) by A0, MYF30;
II0: for x being object holds
( not x in dom f or x = 1 or x = 2 or x = 3 or x = 4 ) by A0, ENUMSET1:def 2;
II: ( 1 in dom f & 2 in dom f & 3 in dom f & 4 in dom f )

proof

dom f = {1,2,3,4} by FUNCT_2:def 1, A0;
hence ( 1 in dom f & 2 in dom f & 3 in dom f & 4 in dom f ) by ENUMSET1:def 2; :: thesis: verum

end;

f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like

proof

set i = eli;
for x being set holds f " x in El_Filtration (eli,MyFunc)

proof

let x be set ; :: thesis: f " x in El_Filtration (eli,MyFunc)
f " x in MyFunc . eli

proof

f " x in bool {1,2,3,4}

proof

per cases ( k1 in x or not k1 in x ) ;

suppose ASUPP1: k1 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k2 in x or not k2 in x ) ;

suppose BSUPP1: k2 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k3 in x or not k3 in x ) ;

suppose CSUPP1: k3 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k4 in x or not k4 in x ) ;

suppose DSUPP1: k4 in x ; :: thesis: f " x in bool {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 ; :: thesis: ( z in {1,2,3,4} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {1,2,3,4} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {1,2,3,4} )

proof

assume z in {1,2,3,4} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then z in dom f by FUNCT_2:def 1, A0;
then consider y being object such that
K01: ( y = f . z & z in dom f ) ;
Fin1: [z,y] in f by K01, FUNCT_1:1;
y in x by K01, A0, ENUMSET1:def 2, A3, ASUPP1, BSUPP1, CSUPP1, DSUPP1;
hence ex y being object st
( [z,y] in f & y in x ) by Fin1; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {1,2,3,4}
( z = 1 or z = 2 or z = 3 or z = 4 ) by U000, FUNCT_1:1, II0;
hence z in {1,2,3,4} by ENUMSET1:def 2; :: thesis: verum

end;

then f " x = {1,2,3,4} by RELAT_1:def 14;
hence f " x in bool {1,2,3,4} ; :: thesis: verum

end;

suppose DSUPP2: not k4 in x ; :: thesis: f " x in bool {1,2,3,4}

for z being object holds
( z in {1,2,3} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {1,2,3} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {1,2,3} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {1,2,3} )

proof

assume z in {1,2,3} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 1 or z = 2 or z = 3 ) by ENUMSET1:def 1;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, ASUPP1, K01, BSUPP1, CSUPP1, SS; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {1,2,3}
z <> 4 by A3, U000, FUNCT_1:1, DSUPP2;
then ( z = 1 or z = 2 or z = 3 ) by U000, FUNCT_1:1, II0;
hence z in {1,2,3} by ENUMSET1:def 1; :: thesis: verum

end;

hence f " x in bool {1,2,3,4} by B123, RELAT_1:def 14; :: thesis: verum

end;

end;

end;

suppose CSUPP2: not k3 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k4 in x or not k4 in x ) ;

suppose DSUPP1: k4 in x ; :: thesis: f " x in bool {1,2,3,4}

for z being object holds
( z in {1,2,4} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {1,2,4} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {1,2,4} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {1,2,4} )

proof

assume z in {1,2,4} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 1 or z = 2 or z = 4 ) by ENUMSET1:def 1;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by SS, A3, ASUPP1, K01, BSUPP1, DSUPP1; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {1,2,4}
z <> 3 by A3, U000, FUNCT_1:1, CSUPP2;
then ( z = 1 or z = 2 or z = 4 ) by II0, U000, FUNCT_1:1;
hence z in {1,2,4} by ENUMSET1:def 1; :: thesis: verum

end;

hence f " x in bool {1,2,3,4} by B124, RELAT_1:def 14; :: thesis: verum

end;

suppose DSUPP2: not k4 in x ; :: thesis: f " x in bool {1,2,3,4}

Fin1: for z being object holds
( z in {1,2} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {1,2} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {1,2} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {1,2} )

proof

assume z in {1,2} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 1 or z = 2 ) by TARSKI:def 2;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, ASUPP1, K01, BSUPP1, SS; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {1,2}
( z <> 3 & z <> 4 ) by A3, U000, FUNCT_1:1, CSUPP2, DSUPP2;
then ( z = 1 or z = 2 ) by U000, FUNCT_1:1, II0;
hence z in {1,2} by TARSKI:def 2; :: thesis: verum

end;

{1,2} in bool {1,2,3,4} by Lm2;
hence f " x in bool {1,2,3,4} by Fin1, RELAT_1:def 14; :: thesis: verum

end;

end;

end;

end;

end;

suppose BSUPP1: not k2 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k3 in x or not k3 in x ) ;

suppose CSUPP1: k3 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k4 in x or not k4 in x ) ;

suppose DSUPP1: k4 in x ; :: thesis: f " x in bool {1,2,3,4}

for z being object holds
( z in {1,3,4} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {1,3,4} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {1,3,4} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {1,3,4} )

proof

assume z in {1,3,4} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 1 or z = 3 or z = 4 ) by ENUMSET1:def 1;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, ASUPP1, K01, SS, CSUPP1, DSUPP1; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {1,3,4}
z <> 2 by A3, U000, FUNCT_1:1, BSUPP1;
then ( z = 1 or z = 3 or z = 4 ) by U000, FUNCT_1:1, II0;
hence z in {1,3,4} by ENUMSET1:def 1; :: thesis: verum

end;

hence f " x in bool {1,2,3,4} by B134, RELAT_1:def 14; :: thesis: verum

end;

suppose DSUPP2: not k4 in x ; :: thesis: f " x in bool {1,2,3,4}

for z being object holds
( z in {1,3} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {1,3} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {1,3} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {1,3} )

proof

assume z in {1,3} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 1 or z = 3 ) by TARSKI:def 2;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, ASUPP1, K01, CSUPP1, SS; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {1,3}
( z <> 2 & z <> 4 ) by A3, U000, FUNCT_1:1, BSUPP1, DSUPP2;
then ( z = 1 or z = 3 ) by U000, FUNCT_1:1, II0;
hence z in {1,3} by TARSKI:def 2; :: thesis: verum

end;

hence f " x in bool {1,2,3,4} by B13, RELAT_1:def 14; :: thesis: verum

end;

end;

end;

suppose CSUPP2: not k3 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k4 in x or not k4 in x ) ;

suppose DSUPP1: k4 in x ; :: thesis: f " x in bool {1,2,3,4}

for z being object holds
( z in {1,4} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {1,4} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {1,4} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {1,4} )

proof

assume z in {1,4} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 1 or z = 4 ) by TARSKI:def 2;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, ASUPP1, K01, SS, DSUPP1; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {1,4}
( z <> 2 & z <> 3 ) by A3, U000, FUNCT_1:1, BSUPP1, CSUPP2;
then ( z = 1 or z = 4 ) by U000, FUNCT_1:1, II0;
hence z in {1,4} by TARSKI:def 2; :: thesis: verum

end;

hence f " x in bool {1,2,3,4} by B14, RELAT_1:def 14; :: thesis: verum

end;

suppose DSUPP2: not k4 in x ; :: thesis: f " x in bool {1,2,3,4}

Fin1: for z being object holds
( z in {1} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {1} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {1} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {1} )

proof

assume K000: z in {1} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then z in dom f by TARSKI:def 1, II;
then consider y being object such that
K01: ( y = f . z & z in dom f ) ;
Fin1: [z,y] in f by K01, FUNCT_1:1;
z = 1 by K000, TARSKI:def 1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, ASUPP1, Fin1, K01; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {1}
( z <> 2 & z <> 3 & z <> 4 ) by A3, FUNCT_1:1, U000, DSUPP2, BSUPP1, CSUPP2;
then z = 1 by U000, FUNCT_1:1, II0;
hence z in {1} by TARSKI:def 1; :: thesis: verum

end;

{1} in bool {1,2,3,4} by EnLm1;
hence f " x in bool {1,2,3,4} by Fin1, RELAT_1:def 14; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose ASUPP2: not k1 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k2 in x or not k2 in x ) ;

suppose BSUPP1: k2 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k3 in x or not k3 in x ) ;

suppose CSUPP1: k3 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k4 in x or not k4 in x ) ;

suppose DSUPP1: k4 in x ; :: thesis: f " x in bool {1,2,3,4}

for z being object holds
( z in {2,3,4} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {2,3,4} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {2,3,4} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {2,3,4} )

proof

assume z in {2,3,4} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 2 or z = 3 or z = 4 ) by ENUMSET1:def 1;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, BSUPP1, K01, SS, CSUPP1, DSUPP1; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {2,3,4}
z <> 1 by A3, FUNCT_1:1, U000, ASUPP2;
then ( z = 2 or z = 3 or z = 4 ) by U000, FUNCT_1:1, II0;
hence z in {2,3,4} by ENUMSET1:def 1; :: thesis: verum

end;

hence f " x in bool {1,2,3,4} by B234, RELAT_1:def 14; :: thesis: verum

end;

suppose DSUPP2: not k4 in x ; :: thesis: f " x in bool {1,2,3,4}

for z being object holds
( z in {2,3} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {2,3} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {2,3} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {2,3} )

proof

assume z in {2,3} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 2 or z = 3 ) by TARSKI:def 2;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, BSUPP1, K01, CSUPP1, SS; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {2,3}
( z <> 1 & z <> 4 ) by A3, U000, FUNCT_1:1, ASUPP2, DSUPP2;
then ( z = 2 or z = 3 ) by U000, FUNCT_1:1, II0;
hence z in {2,3} by TARSKI:def 2; :: thesis: verum

end;

hence f " x in bool {1,2,3,4} by B23, RELAT_1:def 14; :: thesis: verum

end;

end;

end;

suppose CSUPP1: not k3 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k4 in x or not k4 in x ) ;

suppose DSUPP1: k4 in x ; :: thesis: f " x in bool {1,2,3,4}

for z being object holds
( z in {2,4} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {2,4} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {2,4} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {2,4} )

proof

assume z in {2,4} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 2 or z = 4 ) by TARSKI:def 2;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, BSUPP1, K01, DSUPP1, SS; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {2,4}
( z <> 3 & z <> 1 ) by A3, U000, FUNCT_1:1, ASUPP2, CSUPP1;
then ( z = 2 or z = 4 ) by U000, FUNCT_1:1, II0;
hence z in {2,4} by TARSKI:def 2; :: thesis: verum

end;

hence f " x in bool {1,2,3,4} by B24, RELAT_1:def 14; :: thesis: verum

end;

suppose DSUPP2: not k4 in x ; :: thesis: f " x in bool {1,2,3,4}

Fin1: for z being object holds
( z in {2} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {2} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {2} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {2} )

proof

assume K000: z in {2} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then z in dom f by TARSKI:def 1, II;
then consider y being object such that
K01: ( y = f . z & z in dom f ) ;
Fin1: [z,y] in f by K01, FUNCT_1:1;
z = 2 by K000, TARSKI:def 1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, BSUPP1, Fin1, K01; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {2}
( z <> 1 & z <> 3 & z <> 4 ) by A3, U000, FUNCT_1:1, ASUPP2, DSUPP2, CSUPP1;
then z = 2 by U000, FUNCT_1:1, II0;
hence z in {2} by TARSKI:def 1; :: thesis: verum

end;

{2} in bool {1,2,3,4} by EnLm2;
hence f " x in bool {1,2,3,4} by Fin1, RELAT_1:def 14; :: thesis: verum

end;

end;

end;

end;

end;

suppose BSUPP2: not k2 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k3 in x or not k3 in x ) ;

suppose CSUPP1: k3 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k4 in x or not k4 in x ) ;

suppose DSUPP1: k4 in x ; :: thesis: f " x in bool {1,2,3,4}

Fin1: for z being object holds
( z in {3,4} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {3,4} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {3,4} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {3,4} )

proof

assume z in {3,4} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then SS: ( z = 3 or z = 4 ) by TARSKI:def 2;
then consider y being object such that
K01: ( y = f . z & z in dom f ) by II;
[z,y] in f by K01, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, CSUPP1, K01, DSUPP1, SS; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {3,4}
( z <> 1 & z <> 2 ) by A3, U000, FUNCT_1:1, BSUPP2, ASUPP2;
then ( z = 3 or z = 4 ) by U000, FUNCT_1:1, II0;
hence z in {3,4} by TARSKI:def 2; :: thesis: verum

end;

{3,4} in bool {1,2,3,4} by Lm1;
hence f " x in bool {1,2,3,4} by Fin1, RELAT_1:def 14; :: thesis: verum

end;

suppose DSUPP2: not k4 in x ; :: thesis: f " x in bool {1,2,3,4}

Fin1: for z being object holds
( z in {3} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {3} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {3} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {3} )

proof

assume K000: z in {3} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then z in dom f by TARSKI:def 1, II;
then consider y being object such that
K01: ( y = f . z & z in dom f ) ;
Fin1: [z,y] in f by K01, FUNCT_1:1;
z = 3 by K000, TARSKI:def 1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, CSUPP1, Fin1, K01; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {3}
( z <> 1 & z <> 2 & z <> 4 ) by A3, U000, FUNCT_1:1, BSUPP2, DSUPP2, ASUPP2;
then z = 3 by U000, FUNCT_1:1, II0;
hence z in {3} by TARSKI:def 1; :: thesis: verum

end;

{3} in bool {1,2,3,4} by EnLm3;
hence f " x in bool {1,2,3,4} by Fin1, RELAT_1:def 14; :: thesis: verum

end;

end;

end;

suppose CSUPP2: not k3 in x ; :: thesis: f " x in bool {1,2,3,4}

per cases ( k4 in x or not k4 in x ) ;

suppose DSUPP1: k4 in x ; :: thesis: f " x in bool {1,2,3,4}

Fin1: for z being object holds
( z in {4} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {4} iff ex y being object st
( [z,y] in f & y in x ) )
thus ( z in {4} implies ex y being object st
( [z,y] in f & y in x ) ) :: thesis: ( ex y being object st
( [z,y] in f & y in x ) implies z in {4} )

proof

assume K000: z in {4} ; :: thesis: ex y being object st
( [z,y] in f & y in x )
then z in dom f by TARSKI:def 1, II;
then consider y being object such that
K01: ( y = f . z & z in dom f ) ;
Fin1: [z,y] in f by K01, FUNCT_1:1;
z = 4 by K000, TARSKI:def 1;
hence ex y being object st
( [z,y] in f & y in x ) by A3, DSUPP1, Fin1, K01; :: thesis: verum

end;

given y being object such that U000: ( [z,y] in f & y in x ) ; :: thesis: z in {4}
( z <> 1 & z <> 2 & z <> 3 ) by A3, U000, FUNCT_1:1, CSUPP2, ASUPP2, BSUPP2;
then z = 4 by II0, U000, FUNCT_1:1;
hence z in {4} by TARSKI:def 1; :: thesis: verum

end;

{4} in bool {1,2,3,4} by EnLm4;
hence f " x in bool {1,2,3,4} by Fin1, RELAT_1:def 14; :: thesis: verum

end;

suppose DSUPP2: not k4 in x ; :: thesis: f " x in bool {1,2,3,4}

for z being object holds
( z in {} iff ex y being object st
( [z,y] in f & y in x ) )

proof

let z be object ; :: thesis: ( z in {} iff 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 {} )

proof

given y being object such that W1: ( [z,y] in f & y in x ) ; :: thesis: z in {}
( z in dom f & y = f . z ) by W1, FUNCT_1:1;
hence z in {} by A3, W1, ASUPP2, BSUPP2, CSUPP2, DSUPP2, A0, ENUMSET1:def 2; :: thesis: verum

end;

hence ( z in {} iff ex y being object st
( [z,y] in f & y in x ) ) ; :: thesis: verum

end;

then f " x = {} by RELAT_1:def 14;
hence f " x in bool {1,2,3,4} by PROB_1:4; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

hence f " x in MyFunc . eli by A4, A2; :: thesis: verum

end;

hence f " x in El_Filtration (eli,MyFunc) ; :: thesis: verum

end;

hence f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like ; :: thesis: verum

end;

hence ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like ) by A3; :: thesis: verum