reconsider g = f as Element of by YELLOW_1:def 5;
g . i is Element of ;
hence f . i is Element of by FUNCOP_1:13; :: thesis: verum