theorem MYF3: :: FINANCE3:38

for Omega being set st Omega = {1,2,3,4} holds
ex f being Function of Omega,REAL st
( f . 1 = 60 & f . 2 = 80 & f . 3 = 100 & f . 4 = 120 )