reconsider g = f as Element of (product (I --> R)) by YELLOW_1:def 5;
g . i is Element of ((I --> R) . i) ;
hence f . i is Element of R by FUNCOP_1:13; :: thesis: verum