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