reconsider j = 1 as Element of REAL ;
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