:: deftheorem Def3 defines Prj2 TOPALG_5:def 3 :
for S, T, Y being non empty TopSpace
for H being Function of [:S,T:],Y
for s being Point of S
for b₆ being Function of T,Y holds
( b₆ = Prj2 (s,H) iff for t being Point of T holds b₆ . t = H . (s,t) );