let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t being Element of (TermAlg S),s holds A |= t '=' t
let A be non-empty MSAlgebra over S; :: thesis: for s being SortSymbol of S
for t being Element of (TermAlg S),s holds A |= t '=' t
let s be SortSymbol of S; :: thesis: for t being Element of (TermAlg S),s holds A |= t '=' t
let t be Element of (TermAlg S),s; :: thesis: A |= t '=' t
let h be ManySortedFunction of (TermAlg S),A; :: according to EQUATION:def 5 :: thesis: ( not h is_homomorphism TermAlg S,A or (h . s) . ((t '=' t) `1) = (h . s) . ((t '=' t) `2) )
thus ( not h is_homomorphism TermAlg S,A or (h . s) . ((t '=' t) `1) = (h . s) . ((t '=' t) `2) ) ; :: thesis: verum