for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )