let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for B being b₁ -Image MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s st A |= e holds
B |= e
let A be non-empty MSAlgebra over S; :: thesis: for B being A -Image MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s st A |= e holds
B |= e
let B be A -Image MSAlgebra over S; :: thesis: for s being SortSymbol of S
for e being Element of (Equations S) . s st A |= e holds
B |= e
consider f being ManySortedFunction of A,B such that
A1: f is_epimorphism A,B by Def5;
let s be SortSymbol of S; :: thesis: for e being Element of (Equations S) . s st A |= e holds
B |= e
let e be Element of (Equations S) . s; :: thesis: ( A |= e implies B |= e )
assume A2: A |= e ; :: thesis: B |= e
let h be ManySortedFunction of (TermAlg S),B; :: according to EQUATION:def 5 :: thesis: ( not h is_homomorphism TermAlg S,B or (h . s) . (e `1) = (h . s) . (e `2) )
assume A3: h is_homomorphism TermAlg S,B ; :: thesis: (h . s) . (e `1) = (h . s) . (e `2)
consider g being ManySortedFunction of (TermAlg S),A such that
A4: ( g is_homomorphism TermAlg S,A & h = f ** g ) by A1, A3, EQUATION:24;
( h . s = (f . s) * (g . s) & e `1 in the Sorts of (TermAlg S) . s & e `2 in the Sorts of (TermAlg S) . s ) by A4, MSUALG_3:2, EQUATION:29, EQUATION:30;
then ( (h . s) . (e `1) = (f . s) . ((g . s) . (e `1)) & (h . s) . (e `2) = (f . s) . ((g . s) . (e `2)) ) by FUNCT_2:15;
hence (h . s) . (e `1) = (h . s) . (e `2) by A2, A4; :: thesis: verum