let I be set ; :: thesis: for S being non empty non void ManySortedSign
for E being EqualSet of 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 E being EqualSet of 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 EqualSet of 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
let s be SortSymbol of S; :: according to EQUATION:def 6 :: thesis: for e being Element of (Equations S) . s st e in E . s holds
product F |= e
let e be Element of (Equations S) . s; :: thesis: ( e in E . s implies product F |= e )
assume A2: e in E . s ; :: thesis: product F |= e

now :: thesis: for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e )

let i be set ; :: thesis: ( i in I implies ex A being MSAlgebra over S st
( A = F . i & A |= e ) )
assume i in I ; :: thesis: ex A being MSAlgebra over S st
( A = F . i & A |= e )
then consider A being MSAlgebra over S such that
A3: ( A = F . i & A |= E ) by A1;
take A = A; :: thesis: ( A = F . i & A |= e )
thus ( A = F . i & A |= e ) by A2, A3; :: thesis: verum

end;

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