set Omega = {1,2,3,4};
reconsider My80 = 80, My120 = 120 as Element of REAL by NUMBERS:19;
consider f being Function of {1,2,3,4},REAL such that
A3:
( f . 1 = My80 & f . 2 = My80 & f . 3 = My120 & f . 4 = My120 )
by MYF30;
thus
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 )
by A3; verum