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