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 Th32;
reconsider e1 = e `1 as Element of the Sorts of (TermAlg S) . s by Th31;
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

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:25;
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 3
.= (((proj A,i) . s) * (h . s)) . e1 by A3, FUNCT_1:23
.= (((proj A,i) ** h) . s) . e1 by MSUALG_3:2
.= (((proj A,i) ** h) . s) . e2 by A5, A6, Def5
.= (((proj A,i) . s) * (h . s)) . e2 by MSUALG_3:2
.= ((proj A,i) . s) . ((h . s) . e2) by A3, FUNCT_1:23
.= (proj (Carrier A,s),i) . ((h . s) . e2) by PRALG_3:def 3 ; :: thesis: verum

end;

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