:: deftheorem Def5 defines ProjPMap1 MESFUN12:def 5 :
for X1, X2, Y being non empty set
for F being Functional_Sequence of [:X1,X2:],Y
for x being Element of X1
for b₆ being Functional_Sequence of X2,Y holds
( b₆ = ProjPMap1 (F,x) iff for n being Nat holds b₆ . n = ProjPMap1 ((F . n),x) );