let S be non empty non void ManySortedSign ; :: thesis: for X0 being non-empty 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 non-empty countable ManySortedSet of S; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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" ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( t3 = # (t1,w) & t4 = # (t2,w) & A |= t3 '=' t4 implies (h . s) . t1 = (h . s) . t2 )
assume A3: t3 = # (t1,w) ; :: thesis: ( not t4 = # (t2,w) or not A |= t3 '=' t4 or (h . s) . t1 = (h . s) . t2 )
assume A4: t4 = # (t2,w) ; :: thesis: ( not A |= t3 '=' t4 or (h . s) . t1 = (h . s) . t2 )
assume A |= t3 '=' t4 ; :: thesis: (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 ;
:: thesis: verum