let S be non empty non void ManySortedSign ; for U0 being non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s
for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg (U0,R) |= e
let U0 be non-empty MSAlgebra over S; for s being SortSymbol of S
for e being Element of (Equations S) . s
for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg (U0,R) |= e
let s be SortSymbol of S; for e being Element of (Equations S) . s
for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg (U0,R) |= e
let e be Element of (Equations S) . s; for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg (U0,R) |= e
let R be MSCongruence of U0; ( U0 |= e implies QuotMSAlg (U0,R) |= e )
assume A1:
U0 |= e
; QuotMSAlg (U0,R) |= e
set n = (MSNat_Hom (U0,R)) . s;
let h be ManySortedFunction of (TermAlg S),(QuotMSAlg (U0,R)); EQUATION:def 5 ( h is_homomorphism TermAlg S, QuotMSAlg (U0,R) implies (h . s) . (e `1) = (h . s) . (e `2) )
assume
h is_homomorphism TermAlg S, QuotMSAlg (U0,R)
; (h . s) . (e `1) = (h . s) . (e `2)
then consider h0 being ManySortedFunction of (TermAlg S),U0 such that
A2:
h0 is_homomorphism TermAlg S,U0
and
A3:
h = (MSNat_Hom (U0,R)) ** h0
by Th24, MSUALG_4:3;
A4:
dom (h0 . s) = the Sorts of (TermAlg S) . s
by FUNCT_2:def 1;
thus (h . s) . (e `1) =
(((MSNat_Hom (U0,R)) . s) * (h0 . s)) . (e `1)
by A3, MSUALG_3:2
.=
((MSNat_Hom (U0,R)) . s) . ((h0 . s) . (e `1))
by A4, Th29, FUNCT_1:13
.=
((MSNat_Hom (U0,R)) . s) . ((h0 . s) . (e `2))
by A1, A2
.=
(((MSNat_Hom (U0,R)) . s) * (h0 . s)) . (e `2)
by A4, Th30, FUNCT_1:13
.=
(h . s) . (e `2)
by A3, MSUALG_3:2
; verum