let I be set ; :: thesis: for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s
for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e ) ) holds
product F |= e
let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for e being Element of (Equations S) . s
for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e ) ) holds
product F |= e
let s be SortSymbol of S; :: thesis: for e being Element of (Equations S) . s
for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e ) ) holds
product F |= e
let e be Element of (Equations S) . s; :: thesis: for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e ) ) holds
product F |= e
let F be MSAlgebra-Family of I,S; :: thesis: ( ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e ) ) implies product F |= e )
assume A1: for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e ) ; :: thesis: product F |= e

per cases ( I = {} or I <> {} ) ;

suppose I = {} ; :: thesis: product F |= e

then reconsider J = I as empty set ;
reconsider FJ = F as MSAlgebra-Family of J,S ;
thus product F |= e :: thesis: verum

proof

let h be ManySortedFunction of (TermAlg S),(product F); :: according to EQUATION:def 5 :: thesis: ( h is_homomorphism TermAlg S, product F implies (h . s) . (e `1) = (h . s) . (e `2) )
assume h is_homomorphism TermAlg S, product F ; :: thesis: (h . s) . (e `1) = (h . s) . (e `2)
A2: the Sorts of (product FJ) . s = product (Carrier (FJ,s)) by PRALG_2:def 10
.= {{}} by CARD_3:10 ;
A3: (h . s) . (e `2) in the Sorts of (product FJ) . s by Th30, FUNCT_2:5;
(h . s) . (e `1) in the Sorts of (product FJ) . s by Th29, FUNCT_2:5;
hence (h . s) . (e `1) = {} by A2, TARSKI:def 1
.= (h . s) . (e `2) by A2, A3, TARSKI:def 1 ;
:: thesis: verum

end;

end;

suppose I <> {} ; :: thesis: product F |= e

then reconsider J = I as non empty set ;
reconsider F1 = F as MSAlgebra-Family of J,S ;

now :: thesis: for i being Element of J holds F1 . i |= e

let i be Element of J; :: thesis: F1 . i |= e
ex A being MSAlgebra over S st
( A = F1 . i & A |= e ) by A1;
hence F1 . i |= e ; :: thesis: verum

end;

hence product F |= e by Lm1; :: thesis: verum

end;

end;