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