:: deftheorem Def8 defines ProjMap1 MESFUNC9:def 8 :
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₅ = ProjMap1 (F,n) iff for m being Nat holds b₅ . m = F . (n,m) );