reconsider p = f as Element of (product (X --> T)) by YELLOW_1:def 5;
p . x is Element of ((X --> T) . x) ;
hence f . x is Element of T ; :: thesis: verum