UPS (S,T) is SubRelStr of T |^ the carrier of S by Def4;
then reconsider p = f as Element of (T |^ the carrier of S) by YELLOW_0:58;
p . s = p . s ;
hence f . s is Element of T ; :: thesis: verum