:: deftheorem Def9 defines ProjMap2 MESFUNC9:def 9 :
for X, Y being set
for F being Function of [:NAT,NAT:],(PFuncs (X,Y))
for n being Nat
for b₅ being Functional_Sequence of X,Y holds
( b₅ = ProjMap2 (F,n) iff for m being Nat holds b₅ . m = F . (m,n) );