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 ; :: thesis: verum