:: deftheorem defines ProjPMap1 MEASUR13:def 16 :
for n being non zero Nat
for X being non-empty b₁ + 1 -element FinSequence
for f being PartFunc of (CarProduct X),ExtREAL
for x being Element of CarProduct (SubFin (X,n))
for b₅ being PartFunc of (ElmFin (X,(n + 1))),ExtREAL holds
( b₅ = ProjPMap1 (f,x) iff ex g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g & b₅ = ProjPMap1 (g,x) ) );