let k1 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 = 1 ; :: thesis:
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 ; :: 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}}

proof

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

proof

per cases ;

suppose JSUPP1: k1 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:
[z,k1] in f

proof

( z in dom f & k1 = f . z ) by ENUMSET1:def 2, A3, ASSJ0, FUNCT_2:def 1, A0;
hence [z,k1] in f by FUNCT_1:1; :: thesis:

end;

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 {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,3,4} ) by RELAT_1:def 14; :: thesis:

end;

suppose JSUPP2: not k1 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 & not y = k1 ) by M1, FUNCT_1:1, JSUPP2;
hence z in {} by 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,3,4} ) by RELAT_1:def 14; :: thesis:

end;

end;

end;

hence f " x in {{},{1,2,3,4}} by TARSKI: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 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like ) by A3; :: thesis: