let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for B being b1 -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; 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; 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; for e being Element of (Equations S) . s st A |= e holds
B |= e
let e be Element of (Equations S) . s; ( A |= e implies B |= e )
assume A2:
A |= e
; B |= e
let h be ManySortedFunction of (TermAlg S),B; EQUATION:def 5 ( not h is_homomorphism TermAlg S,B or (h . s) . (e `1) = (h . s) . (e `2) )
assume A3:
h is_homomorphism TermAlg S,B
; (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; verum