let S be non empty non void ManySortedSign ; for X0 being V5() countable ManySortedSet of S
for B being non-empty MSAlgebra over S
for h being ManySortedFunction of (Free (S,X0)),B st h is_homomorphism Free (S,X0),B holds
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & B |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2
let X0 be V5() countable ManySortedSet of S; for B being non-empty MSAlgebra over S
for h being ManySortedFunction of (Free (S,X0)),B st h is_homomorphism Free (S,X0),B holds
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & B |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2
let A be non-empty MSAlgebra over S; for h being ManySortedFunction of (Free (S,X0)),A st h is_homomorphism Free (S,X0),A holds
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & A |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2
let h be ManySortedFunction of (Free (S,X0)),A; ( h is_homomorphism Free (S,X0),A implies for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & A |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2 )
assume A1:
h is_homomorphism Free (S,X0),A
; for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & A |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2
let w be ManySortedFunction of X0, the carrier of S --> NAT; ( w is "1-1" implies for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & A |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2 )
assume
w is "1-1"
; for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & A |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2
then consider g being ManySortedFunction of (TermAlg S),(Free (S,X0)) such that
A2:
( g is_homomorphism TermAlg S, Free (S,X0) & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t ) )
by Th73;
let s be SortSymbol of S; for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & A |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2
let t1, t2 be Element of (Free (S,X0)),s; for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & A |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2
let t3, t4 be Element of (TermAlg S),s; ( t3 = # (t1,w) & t4 = # (t2,w) & A |= t3 '=' t4 implies (h . s) . t1 = (h . s) . t2 )
assume A3:
t3 = # (t1,w)
; ( not t4 = # (t2,w) or not A |= t3 '=' t4 or (h . s) . t1 = (h . s) . t2 )
assume A4:
t4 = # (t2,w)
; ( not A |= t3 '=' t4 or (h . s) . t1 = (h . s) . t2 )
assume
A |= t3 '=' t4
; (h . s) . t1 = (h . s) . t2
then A6:
((h ** g) . s) . ((t3 '=' t4) `1) = ((h ** g) . s) . ((t3 '=' t4) `2)
by A2, A1, MSUALG_3:10;
(h ** g) . s = (h . s) * (g . s)
by MSUALG_3:2;
then
( ((h ** g) . s) . t3 = (h . s) . ((g . s) . t3) & ((h ** g) . s) . t4 = (h . s) . ((g . s) . t4) )
by FUNCT_2:15;
hence (h . s) . t1 =
(h . s) . ((g . s) . t4)
by A2, A6, A3
.=
(h . s) . t2
by A2, A4
;
verum