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 U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds
U2 |= 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 U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds
U2 |= e
let s be SortSymbol of S; :: thesis: for e being Element of (Equations S) . s
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds
U2 |= e
let e be Element of (Equations S) . s; :: thesis: for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds
U2 |= e
let U2 be strict non-empty MSSubAlgebra of U0; :: thesis: ( U0 |= e implies U2 |= e )
assume A1: U0 |= e ; :: thesis: U2 |= e
let h be ManySortedFunction of (TermAlg S),U2; :: according to EQUATION:def 5 :: thesis: ( h is_homomorphism TermAlg S,U2 implies (h . s) . (e `1) = (h . s) . (e `2) )
assume A2: h is_homomorphism TermAlg S,U2 ; :: thesis: (h . s) . (e `1) = (h . s) . (e `2)
A3: the Sorts of (TermAlg S) is_transformable_to the Sorts of U2 ;
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 9;
then reconsider f1 = h as ManySortedFunction of (TermAlg S),U0 by A3, EXTENS_1:5;
f1 is_homomorphism TermAlg S,U0 by A2, MSUALG_9:15;
hence (h . s) . (e `1) = (h . s) . (e `2) by A1; :: thesis: verum