theorem MYF30: :: FINANCE3:34

for k1, k2, k3, k4 being 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 )