let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg (U0,R) |= e
let R be MSCongruence of U0; :: thesis: ( U0 |= e implies QuotMSAlg (U0,R) |= e )
assume A1: U0 |= e ; :: thesis: QuotMSAlg (U0,R) |= e
set n = (MSNat_Hom (U0,R)) . s;
let h be ManySortedFunction of (TermAlg S),(QuotMSAlg (U0,R)); :: according to EQUATION:def 5 :: thesis: ( 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) ; :: thesis: (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 ; :: thesis: verum