let Omega be set ; :: thesis: ( Omega = {1,2,3,4} implies ex f being Function of Omega,REAL st
( f . 1 = 60 & f . 2 = 80 & f . 3 = 100 & f . 4 = 120 ) )
assume A1: Omega = {1,2,3,4} ; :: thesis: ex f being Function of Omega,REAL st
( f . 1 = 60 & f . 2 = 80 & f . 3 = 100 & f . 4 = 120 )
reconsider My60 = 60, My80 = 80 as Element of REAL by NUMBERS:19;
reconsider My100 = 100, My120 = 120 as Element of REAL by NUMBERS:19;
consider f being Function of Omega,REAL such that
A3: ( f . 1 = My60 & f . 2 = My80 & f . 3 = My100 & f . 4 = My120 ) by A1, MYF30;
thus ex f being Function of Omega,REAL st
( f . 1 = 60 & f . 2 = 80 & f . 3 = 100 & f . 4 = 120 ) by A3; :: thesis: verum