reconsider j = 1 as Element of REAL by XREAL_0:def 1;
take NAT --> j ; :: thesis: ( (NAT --> j) . 0 = 1 & ( for n being Element of NAT holds (NAT --> j) . n >= 0 ) )
thus ( (NAT --> j) . 0 = 1 & ( for n being Element of NAT holds (NAT --> j) . n >= 0 ) ) by FUNCOP_1:7; :: thesis: verum