set k = the Element of Omega2;
set z = Omega --> the Element of Omega2;
A1: ( Omega --> the Element of Omega2 is F,F2 -random_variable-like iff for x being set st x in F2 holds
(Omega --> the Element of Omega2) " x in F ) ;
for x being Element of F2 holds (Omega --> the Element of Omega2) " x in F

let x be Element of F2; :: thesis:
set K = (Omega --> the Element of Omega2) " x;
A2: dom (Omega --> the Element of Omega2) = Omega by FUNCT_2:def 1;

for s being object holds
( s in (Omega --> the Element of Omega2) " x iff s in Omega )

let s be object ; :: thesis:
thus ( s in (Omega --> the Element of Omega2) " x implies s in Omega ) ; :: thesis:
assume s in Omega ; :: thesis:
then ( s in Omega & (Omega --> the Element of Omega2) . s in x ) by A3, FUNCOP_1:7;
hence s in (Omega --> the Element of Omega2) " x by A2, FUNCT_1:def 7; :: thesis:

end;

then (Omega --> the Element of Omega2) " x = Omega by TARSKI:2;
then (Omega --> the Element of Omega2) " x is Element of F by PROB_1:23;
hence (Omega --> the Element of Omega2) " x in F ; :: thesis:

end;

for r being object holds not r in (Omega --> the Element of Omega2) " x

let r be object ; :: thesis:
assume r in (Omega --> the Element of Omega2) " x ; :: thesis:
then ( r in dom (Omega --> the Element of Omega2) & (Omega --> the Element of Omega2) . r in x ) by FUNCT_1:def 7;
hence contradiction by A4, FUNCOP_1:7; :: thesis:

end;

end;

end;