set Omega = {1,2,3,4};
reconsider My100 = 100 as Element of REAL by NUMBERS:19;
consider f being Function of {1,2,3,4},REAL such that
A3: ( f . 1 = My100 & f . 2 = My100 & f . 3 = My100 & f . 4 = My100 ) by MYF30;
thus for Omega being set st Omega = {1,2,3,4} holds
ex f being Function of Omega,REAL st
( f . 1 = 100 & f . 2 = 100 & f . 3 = 100 & f . 4 = 100 ) by A3; :: thesis: verum