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, 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; :: thesis: 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; :: thesis: 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; :: thesis: ( A |= t1 '=' t2 & A |= t2 '=' t3 implies A |= t1 '=' t3 )
assume A1: ( A |= t1 '=' t2 & A |= t2 '=' t3 ) ; :: thesis: A |= t1 '=' t3
let h be ManySortedFunction of (TermAlg S),A; :: according to EQUATION:def 5 :: thesis: ( 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 ; :: thesis: (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) ; :: thesis: verum