let k1, k2, k3, k4 be Element of REAL ; :: thesis:
let Omega be set ; :: thesis:
assume ASS: Omega = {1,2,3,4} ; :: thesis:
A1: 1 in Omega by ENUMSET1:def 2, ASS;
A2: 2 in Omega by ENUMSET1:def 2, ASS;
A3: 3 in Omega by ENUMSET1:def 2, ASS;
A4: 4 in Omega by ENUMSET1:def 2, ASS;
reconsider Omega = Omega as non empty set by ASS;
deffunc H₁( Element of Omega) -> Element of REAL = Set2_for_RandomVariable (k1,k2,k3,k4,$1);
consider f being Function of Omega,REAL such that
B1: for d being Element of Omega holds f . d = H₁(d) from FUNCT_2:sch 4();
B2: f . 1 = k1

consider k being Element of Omega such that
C1: k = 1 by A1;
f . k = Set2_for_RandomVariable (k1,k2,k3,k4,k) by B1;
hence f . 1 = k1 by C1, Def77; :: thesis:

end;

B3: f . 2 = k2

consider k being Element of Omega such that
C1: k = 2 by A2;
( f . 2 = Set2_for_RandomVariable (k1,k2,k3,k4,k) & k = 2 ) by B1, C1;
then ( f . 2 = Set3_for_RandomVariable (k2,k3,k4,k) & k = 2 ) by Def77;
hence f . 2 = k2 by Def78; :: thesis:

end;

B4: f . 3 = k3

consider k being Element of Omega such that
C1: k = 3 by A3;
f . k = Set2_for_RandomVariable (k1,k2,k3,k4,k) by B1;
then ( f . 3 = Set3_for_RandomVariable (k2,k3,k4,k) & k = 3 ) by C1, Def77;
then ( f . 3 = Set4_for_RandomVariable (k3,k4,k) & k = 3 ) by Def78;
hence f . 3 = k3 by Def79; :: thesis:

end;

f . 4 = k4

consider k being Element of Omega such that
C1: k = 4 by A4;
f . k = Set2_for_RandomVariable (k1,k2,k3,k4,k) by B1;
then ( f . 4 = Set3_for_RandomVariable (k2,k3,k4,k) & k = 4 ) by C1, Def77;
then ( f . 4 = Set4_for_RandomVariable (k3,k4,k) & k = 4 ) by Def78;
hence f . 4 = k4 by Def79; :: thesis:

end;

hence ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 ) by B2, B3, B4; :: thesis: