let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for e being Element of (Equations S) . s
for I being non empty set
for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e
let s be SortSymbol of S; :: thesis: for e being Element of (Equations S) . s
for I being non empty set
for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e
let e be Element of (Equations S) . s; :: thesis: for I being non empty set
for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e
reconsider e2 = e `2 as Element of the Sorts of (TermAlg S) . s by Th30;
reconsider e1 = e `1 as Element of the Sorts of (TermAlg S) . s by Th29;
let I be non empty set ; :: thesis: for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e
let A be MSAlgebra-Family of I,S; :: thesis: ( ( for i being Element of I holds A . i |= e ) implies product A |= e )
assume A1: for i being Element of I holds A . i |= e ; :: thesis: product A |= e
let h be ManySortedFunction of (TermAlg S),(product A); :: according to EQUATION:def 5 :: thesis: ( h is_homomorphism TermAlg S, product A implies (h . s) . (e `1) = (h . s) . (e `2) )
assume A2: h is_homomorphism TermAlg S, product A ; :: thesis: (h . s) . (e `1) = (h . s) . (e `2)
A3: dom (h . s) = the Sorts of (TermAlg S) . s by FUNCT_2:def 1;

A4: now :: thesis: for i being Element of I holds (proj ((Carrier (A,s)),i)) . ((h . s) . e1) = (proj ((Carrier (A,s)),i)) . ((h . s) . e2)

let i be Element of I; :: thesis: (proj ((Carrier (A,s)),i)) . ((h . s) . e1) = (proj ((Carrier (A,s)),i)) . ((h . s) . e2)
set Z = (proj (A,i)) ** h;
A5: A . i |= e by A1;
proj (A,i) is_homomorphism product A,A . i by PRALG_3:24;
then A6: (proj (A,i)) ** h is_homomorphism TermAlg S,A . i by A2, MSUALG_3:10;
thus (proj ((Carrier (A,s)),i)) . ((h . s) . e1) = ((proj (A,i)) . s) . ((h . s) . e1) by PRALG_3:def 2
.= (((proj (A,i)) . s) * (h . s)) . e1 by A3, FUNCT_1:13
.= (((proj (A,i)) ** h) . s) . e1 by MSUALG_3:2
.= (((proj (A,i)) ** h) . s) . e2 by A5, A6
.= (((proj (A,i)) . s) * (h . s)) . e2 by MSUALG_3:2
.= ((proj (A,i)) . s) . ((h . s) . e2) by A3, FUNCT_1:13
.= (proj ((Carrier (A,s)),i)) . ((h . s) . e2) by PRALG_3:def 2 ; :: thesis: verum

end;

the Sorts of (product A) . s = product (Carrier (A,s)) by PRALG_2:def 10;
hence (h . s) . (e `1) = (h . s) . (e `2) by A4, MSUALG_9:14; :: thesis: verum