let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty trivial MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s holds A |= e
let A be non-empty trivial MSAlgebra over S; :: thesis: for s being SortSymbol of S
for e being Element of (Equations S) . s holds A |= e
let s be SortSymbol of S; :: thesis: for e being Element of (Equations S) . s holds A |= e
let e be Element of (Equations S) . s; :: thesis: A |= e
let h be ManySortedFunction of (TermAlg S),A; :: according to EQUATION:def 5 :: thesis: ( not h is_homomorphism TermAlg S,A or (h . s) . (e `1) = (h . s) . (e `2) )
assume h is_homomorphism TermAlg S,A ; :: thesis: (h . s) . (e `1) = (h . s) . (e `2)
( (h . s) . (e `1) in the Sorts of A . s & (h . s) . (e `2) in the Sorts of A . s ) by FUNCT_2:5, EQUATION:30, EQUATION:29;
hence (h . s) . (e `1) = (h . s) . (e `2) by ZFMISC_1:def 10; :: thesis: verum