:: deftheorem Def6 defines ProjPMap2 MESFUN12:def 6 :
for X1, X2, Y being non empty set
for F being Functional_Sequence of [:X1,X2:],Y
for y being Element of X2
for b₆ being Functional_Sequence of X1,Y holds
( b₆ = ProjPMap2 (F,y) iff for n being Nat holds b₆ . n = ProjPMap2 ((F . n),y) );