let k1, k2, k3, k4 be Element of REAL ; for Omega being set st Omega = {1,2,3,4} holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 )
let Omega be set ; ( Omega = {1,2,3,4} implies ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 ) )
assume ASS:
Omega = {1,2,3,4}
; ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 )
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 H1( 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 = H1(d)
from FUNCT_2:sch 4();
B2:
f . 1 = k1
B3:
f . 2 = k2
B4:
f . 3 = k3
proof
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;
verum
end;
f . 4 = k4
proof
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;
verum
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; verum