theorem :: PRALG_3:24

for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i