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