theorem MYF20: :: FINANCE3:37

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