let k1, k2 be Element of REAL ; :: thesis:
let Omega be non empty set ; :: thesis:
assume A0: Omega = {1,2,3,4} ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let I be non empty real-membered set ; :: thesis:
let MyFunc be ManySortedSigmaField of I,Sigma; :: thesis:
assume A2: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} ) ; :: thesis:
let eli be Element of I; :: thesis:
assume A4: eli = 2 ; :: thesis:
consider f being Function of Omega,REAL such that
A3: ( f . 1 = k1 & f . 2 = k1 & f . 3 = k2 & f . 4 = k2 ) by A0, MYF30;
take f ; :: thesis:
set i = eli;
for x being set holds f " x in El_Filtration (eli,MyFunc)

proof

let x be set ; :: thesis:
f " x in MyFunc . eli

proof

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

proof

( f " x = {} or f " x = {1,2} or f " x = {3,4} or f " x = {1,2,3,4} )

proof

per cases ;

suppose INITSUPP: k1 in x ; :: thesis:

per cases ;

suppose JSUPP1: k2 in x ; :: thesis:

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:
I1: ( z in {1,2,3,4} implies ex y being object st
( [z,y] in f & y in x ) )

proof

assume ASSJ0: z in {1,2,3,4} ; :: thesis:
then L1: z in dom f by FUNCT_2:def 1, A0;

per cases by ASSJ0, ENUMSET1:def 2;

suppose ( z = 1 or z = 2 ) ; :: thesis:

then ( [z,k1] in f & k1 in x ) by A3, INITSUPP, L1, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) ; :: thesis:

end;

suppose ( z = 3 or z = 4 ) ; :: thesis:

then ( f . z = k2 & k2 in x & z in dom f ) by A3, JSUPP1, ASSJ0, FUNCT_2:def 1, A0;
then ( [z,k2] in f & k2 in x ) by FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) ; :: thesis:

end;

end;

end;

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

proof

given y being object such that ASSJ0: ( [z,y] in f & y in x ) ; :: thesis:
( z in dom f & y = f . z ) by ASSJ0, FUNCT_1:1;
hence z in {1,2,3,4} by A0; :: thesis:

end;

hence ( z in {1,2,3,4} iff ex y being object st
( [z,y] in f & y in x ) ) by I1; :: thesis:

end;

hence ( f " x = {} or f " x = {1,2} or f " x = {3,4} or f " x = {1,2,3,4} ) by RELAT_1:def 14; :: thesis:

end;

suppose JSUPP2: not k2 in x ; :: thesis:

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:
I1: ( z in {1,2} implies ex y being object st
( [z,y] in f & y in x ) )

proof

assume z in {1,2} ; :: thesis:
then S2: ( z = 1 or z = 2 ) by TARSKI:def 2;
then z in Omega by ENUMSET1:def 2, A0;
then S1: z in dom f by FUNCT_2:def 1;
[z,k1] in f by S1, S2, A3, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by INITSUPP; :: thesis:

end;

( ex y being object st
( [z,y] in f & y in x ) implies z in {1,2} )

proof

given y being object such that M1: ( [z,y] in f & y in x ) ; :: thesis:
z in dom f by M1, FUNCT_1:1;
then ( z = 1 or z = 2 or z = 3 or z = 4 ) by A0, ENUMSET1:def 2;
hence z in {1,2} by JSUPP2, M1, FUNCT_1:1, A3, TARSKI:def 2; :: thesis:

end;

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

end;

hence ( f " x = {} or f " x = {1,2} or f " x = {3,4} or f " x = {1,2,3,4} ) by RELAT_1:def 14; :: thesis:

end;

end;

end;

suppose INITSUPP: not k1 in x ; :: thesis:

per cases ;

suppose JSUPP1: k2 in x ; :: thesis:

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:
I1: ( z in {3,4} implies ex y being object st
( [z,y] in f & y in x ) )

proof

assume z in {3,4} ; :: thesis:
then J1: ( z = 3 or z = 4 ) by TARSKI:def 2;
then z in {1,2,3,4} by ENUMSET1:def 2;
then z in dom f by FUNCT_2:def 1, A0;
then [z,k2] in f by J1, A3, FUNCT_1:1;
hence ex y being object st
( [z,y] in f & y in x ) by JSUPP1; :: thesis:

end;

( ex y being object st
( [z,y] in f & y in x ) implies z in {3,4} )

proof

given y being object such that ASSJ0: ( [z,y] in f & y in x ) ; :: thesis:
OO0: ( y = k1 or y = k2 )

proof

z in dom f by ASSJ0, FUNCT_1:1;
then ( z = 1 or z = 2 or z = 3 or z = 4 ) by ENUMSET1:def 2, A0;
hence ( y = k1 or y = k2 ) by A3, ASSJ0, FUNCT_1:1; :: thesis:

end;

Z10: k2 = f . z

proof

per cases by OO0;

suppose y = k1 ; :: thesis:

hence k2 = f . z by INITSUPP, ASSJ0; :: thesis:

end;

suppose y = k2 ; :: thesis:

hence k2 = f . z by ASSJ0, FUNCT_1:1; :: thesis:

end;

end;

end;

( z = 3 or z = 4 )

proof

assume ZZ1: ( z <> 3 & z <> 4 ) ; :: thesis:
z in dom f by ASSJ0, FUNCT_1:1;
hence contradiction by Z10, ZZ1, A3, INITSUPP, JSUPP1, ENUMSET1:def 2, A0; :: thesis:

end;

hence z in {3,4} by TARSKI:def 2; :: thesis:

end;

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

end;

hence ( f " x = {} or f " x = {1,2} or f " x = {3,4} or f " x = {1,2,3,4} ) by RELAT_1:def 14; :: thesis:

end;

suppose JSUPP2: not k2 in x ; :: thesis:

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:
( ex y being object st
( [z,y] in f & y in x ) implies z in {} )

proof

given y being object such that M1: ( [z,y] in f & y in x ) ; :: thesis:
( z in dom f & y = f . z & y <> k2 ) by M1, FUNCT_1:1, JSUPP2;
hence z in {} by INITSUPP, M1, A3, A0, ENUMSET1:def 2; :: thesis:

end;

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

end;

hence ( f " x = {} or f " x = {1,2} or f " x = {3,4} or f " x = {1,2,3,4} ) by RELAT_1:def 14; :: thesis:

end;

end;

end;

end;

end;

hence f " x in {{},{1,2},{3,4},{1,2,3,4}} by ENUMSET1:def 2; :: thesis:

end;

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

end;

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

end;

hence ( f . 1 = k1 & f . 2 = k1 & f . 3 = k2 & f . 4 = k2 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like ) by A3; :: thesis: