let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of 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 of 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
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 A2: h is_homomorphism TermAlg S, QuotMSAlg U0,R ; :: thesis: (h . s) . (e `1 ) = (h . s) . (e `2 )
MSNat_Hom U0,R is_epimorphism U0, QuotMSAlg U0,R by MSUALG_4:3;
then consider h0 being ManySortedFunction of (TermAlg S),U0 such that
A3: h0 is_homomorphism TermAlg S,U0 and
A4: h = (MSNat_Hom U0,R) ** h0 by A2, Th26;
set n = (MSNat_Hom U0,R) . s;
A5: 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 A4, MSUALG_3:2
.= ((MSNat_Hom U0,R) . s) . ((h0 . s) . (e `1 )) by A5, Th31, FUNCT_1:23
.= ((MSNat_Hom U0,R) . s) . ((h0 . s) . (e `2 )) by A1, A3, Def5
.= (((MSNat_Hom U0,R) . s) * (h0 . s)) . (e `2 ) by A5, Th32, FUNCT_1:23
.= (h . s) . (e `2 ) by A4, MSUALG_3:2 ; :: thesis: verum