:: deftheorem Def2 defines proj PRALG_3:def 2 :
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for b₅ being ManySortedFunction of (product A),(A . i) holds
( b₅ = proj (A,i) iff for s being Element of S holds b₅ . s = proj ((Carrier (A,s)),i) );