let S be non empty non void ManySortedSign ; for U0, U1 being non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds
U1 |= e
let U0, U1 be non-empty MSAlgebra over S; for s being SortSymbol of S
for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds
U1 |= e
let s be SortSymbol of S; for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds
U1 |= e
let e be Element of (Equations S) . s; ( U0,U1 are_isomorphic & U0 |= e implies U1 |= e )
assume that
A1:
U0,U1 are_isomorphic
and
A2:
U0 |= e
; U1 |= e
consider F being ManySortedFunction of U0,U1 such that
A3:
F is_isomorphism U0,U1
by A1;
consider G being ManySortedFunction of U1,U0 such that
A4:
G = F ""
;
( F is "1-1" & F is "onto" )
by A3, MSUALG_3:13;
then A5:
G . s = (F . s) "
by A4, MSUALG_3:def 4;
F is "onto"
by A3, MSUALG_3:13;
then A6:
rng (F . s) = the Sorts of U1 . s
;
let h1 be ManySortedFunction of (TermAlg S),U1; EQUATION:def 5 ( h1 is_homomorphism TermAlg S,U1 implies (h1 . s) . (e `1) = (h1 . s) . (e `2) )
assume A7:
h1 is_homomorphism TermAlg S,U1
; (h1 . s) . (e `1) = (h1 . s) . (e `2)
set F1 = G ** h1;
G is_isomorphism U1,U0
by A3, A4, MSUALG_3:14;
then
G is_homomorphism U1,U0
by MSUALG_3:13;
then A8:
G ** h1 is_homomorphism TermAlg S,U0
by A7, MSUALG_3:10;
F is "1-1"
by A3, MSUALG_3:13;
then A9:
F . s is one-to-one
by MSUALG_3:1;
(G ** h1) . s = (G . s) * (h1 . s)
by MSUALG_3:2;
then A10: (F . s) * ((G ** h1) . s) =
((F . s) * (G . s)) * (h1 . s)
by RELAT_1:36
.=
(id ( the Sorts of U1 . s)) * (h1 . s)
by A5, A6, A9, FUNCT_2:29
.=
h1 . s
by FUNCT_2:17
;
A11:
dom ((G ** h1) . s) = the Sorts of (TermAlg S) . s
by FUNCT_2:def 1;
hence (h1 . s) . (e `1) =
(F . s) . (((G ** h1) . s) . (e `1))
by A10, Th29, FUNCT_1:13
.=
(F . s) . (((G ** h1) . s) . (e `2))
by A2, A8
.=
(h1 . s) . (e `2)
by A10, A11, Th30, FUNCT_1:13
;
verum